MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen Structured version   GIF version

Theorem rgen 2814
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1 (𝑥𝐴𝜑)
Assertion
Ref Expression
rgen 𝑥𝐴 𝜑

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2753 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1566 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1734  wral 2748
This theorem is referenced by:  rgen2a  2815  rgenw  2816  mprg  2818  mprgbir  2819  rgen2  2845  r19.21be  2850  nrex  2851  rexlimi  2866  sbcth2  3303  reuss  3651  r19.2zb  3788  ral0  3802  unimax  4128  mpteq1  4373  mpteq2ia  4375  reusv2lem4  4819  onssmin  4869  tfis  4926  omssnlim  4951  finds  4963  finds2  4965  fnopab  5668  fmpti  5992  opabex3  6090  sorpssuni  6635  sorpssint  6636  seqomlem2  6803  findcard3  7445  fifo  7532  fisupcl  7567  dfom3  7697  cantnfvalf  7715  rankf  7815  scottex  7906  cplem1  7910  harcard  7962  cardiun  7966  r0weon  7991  acnnum  8030  alephon  8047  alephsmo  8080  alephf1ALT  8081  alephfplem4  8085  dfac5lem4  8104  dfacacn  8118  kmlem1  8127  cflem  8223  cflecard  8230  cfsmolem  8247  fin23lem17  8315  hsmexlem4  8406  omina  8663  0tsk  8727  inar1  8747  wfgru  8788  reclem2pr  9022  nnssre  10102  dfnn2  10111  dfnn3  10112  nnind  10116  nnsub  10136  dfuzi  10458  uzinfmi  10655  uzsupss  10668  cnref1o  10707  xrsupsslem  10985  xrinfmsslem  10986  xrsup0  11002  ser0f  11480  bccl  11717  hashkf  11724  hashbc  11806  wrdind  11901  sqrlem5  12172  rexuz3  12272  sqrf  12287  ackbijnn  12727  incexclem  12736  eff2  12820  reeff1  12841  sqr2irr  12968  prmind2  13210  3prm  13216  pockthi  13395  infpn2  13401  prminf  13403  prmreclem2  13405  prmrec  13410  1arith  13415  1arith2  13416  vdwlem13  13481  ramz  13513  prmlem1a  13549  xpsff1o  13913  isacs1i  14002  dmaf  14324  cdaf  14325  coapm  14346  lublecllem  14565  odf  15307  efgrelexlemb  15514  dprd2da  15732  mgpf  15807  prdscrngd  15851  cnfld1  16858  cnsubglem  16879  cnmsubglem  16893  isbasis3g  17146  basdif0  17150  distop  17192  mretopd  17288  2ndcsep  17654  kqf  17911  fbssfi  18001  filcon  18047  prdstmdd  18285  ustfilxp  18374  prdsxmslem2  18691  qdensere  18936  recld2  18977  ovolf  19510  dyadmax  19622  dveflem  19995  mdegxrf  20123  fta1  20357  vieta1  20361  aalioulem2  20382  taylfval  20407  pilem2  20500  pilem3  20501  recosf1o  20569  divlogrlim  20658  logcn  20670  ressatans  20906  leibpi  20914  ftalem3  20989  chtub  21128  2sqlem6  21285  2sqlem10  21290  chtppilim  21301  pntpbnd1  21412  pntlem3  21435  padicabvf  21457  isgrpoi  21918  cnid  22071  mulid  22076  cnrngo  22123  isvci  22193  isnvi  22224  ipasslem8  22470  hilid  22795  hlimf  22872  shsspwh  22880  pjrni  23336  pjmf1  23350  df0op2  23387  dfiop2  23388  hoaddcomi  23407  hoaddassi  23411  hocadddiri  23414  hocsubdiri  23415  hoaddid1i  23421  ho0coi  23423  hoid1i  23424  hoid1ri  23425  honegsubi  23431  hoddii  23624  lnopunilem2  23646  elunop2  23648  lnophm  23654  imaelshi  23693  cnlnadjlem8  23709  pjnmopi  23783  pjsdii  23790  pjddii  23791  pjtoi  23814  chirred  24030  nnindf  24337  nn0min  24338  nn0srg  24489  rge0srg  24490  rearchi  24607  cnzh  24697  rezh  24698  dmvlsiga  24870  volmeas  24945  ddemeas  24950  sxbrsigalem3  24985  eulerpartlemsf  25034  eulerpartlemgh  25053  coinfliprv  25133  ballotlem7  25186  signsw0glem  25223  signsvvf  25249  kur14lem9  25366  prodf1f  25677  dfon2lem7  25873  epsetlike  25926  wfisg  25941  frinsg  25977  wfr3  26013  tfrALTlem  26014  bdayfo  26087  nodense  26101  fobigcup  26202  axcontlem2  26361  onsucsuccmpi  26650  heicant  26695  mblfinlem1  26697  volsupnfl  26705  dvtan  26711  itg2addnc  26715  nn0prpwlem  26781  refref  26821  topmeet  26849  indexa  26891  sstotbnd2  26939  heiborlem7  26982  mzpclall  27308  dgraaf  27851  phisum  28017  stoweidlem57  28300  wallispilem3  28310  stirlinglem13  28329  wwlktovfun  28802  bnj580  30252  bnj1384  30369  bnj1497  30397  atpsubN  31599  idldil  31960  cdleme50ldil  32394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562
This theorem depends on definitions:  df-bi 179  df-ral 2753
  Copyright terms: Public domain W3C validator