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

Theorem rgen 2778
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 2717 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1560 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1728  wral 2712
This theorem is referenced by:  rgen2a  2779  rgenw  2780  mprg  2782  mprgbir  2783  rgen2  2809  r19.21be  2814  nrex  2815  rexlimi  2830  sbcth2  3263  reuss  3610  r19.2zb  3746  ral0  3760  unimax  4078  mpteq1  4320  mpteq2ia  4322  reusv2lem4  4762  onssmin  4812  tfis  4869  omssnlim  4894  finds  4906  finds2  4908  fnopab  5604  fmpti  5928  opabex3  6026  sorpssuni  6567  sorpssint  6568  seqomlem2  6744  findcard3  7386  fifo  7473  fisupcl  7508  dfom3  7638  cantnfvalf  7656  rankf  7756  scottex  7847  cplem1  7851  harcard  7903  cardiun  7907  r0weon  7932  acnnum  7971  alephon  7988  alephsmo  8021  alephf1ALT  8022  alephfplem4  8026  dfac5lem4  8045  dfacacn  8059  kmlem1  8068  cflem  8164  cflecard  8171  cfsmolem  8188  fin23lem17  8256  hsmexlem4  8347  omina  8604  0tsk  8668  inar1  8688  wfgru  8729  reclem2pr  8963  nnssre  10042  dfnn2  10051  dfnn3  10052  nnind  10056  nnsub  10076  dfuzi  10398  uzinfmi  10593  uzsupss  10606  cnref1o  10645  xrsupsslem  10923  xrinfmsslem  10924  xrsup0  10940  ser0f  11414  bccl  11651  hashkf  11658  hashbc  11740  wrdind  11829  sqrlem5  12090  rexuz3  12190  sqrf  12205  ackbijnn  12645  incexclem  12654  eff2  12738  reeff1  12759  sqr2irr  12886  prmind2  13128  3prm  13134  pockthi  13313  infpn2  13319  prminf  13321  prmreclem2  13323  prmrec  13328  1arith  13333  1arith2  13334  vdwlem13  13399  ramz  13431  prmlem1a  13467  xpsff1o  13831  isacs1i  13920  dmaf  14242  cdaf  14243  coapm  14264  lubid  14477  odf  15213  efgrelexlemb  15420  dprd2da  15638  mgpf  15713  prdscrngd  15757  cnfld1  16764  cnsubglem  16785  cnmsubglem  16799  isbasis3g  17052  basdif0  17056  distop  17098  mretopd  17194  2ndcsep  17560  kqf  17817  fbssfi  17907  filcon  17953  prdstmdd  18191  ustfilxp  18280  prdsxmslem2  18597  qdensere  18842  recld2  18883  ovolf  19416  dyadmax  19528  dveflem  19901  mdegxrf  20029  fta1  20263  vieta1  20267  aalioulem2  20288  taylfval  20313  pilem2  20406  pilem3  20407  recosf1o  20475  divlogrlim  20564  logcn  20576  ressatans  20812  leibpi  20820  ftalem3  20895  chtub  21034  2sqlem6  21191  2sqlem10  21196  chtppilim  21207  pntpbnd1  21318  pntlem3  21341  padicabvf  21363  isgrpoi  21824  cnid  21977  mulid  21982  cnrngo  22029  isvci  22099  isnvi  22130  ipasslem8  22376  hilid  22701  hlimf  22778  shsspwh  22786  pjrni  23242  pjmf1  23256  df0op2  23293  dfiop2  23294  hoaddcomi  23313  hoaddassi  23317  hocadddiri  23320  hocsubdiri  23321  hoaddid1i  23327  ho0coi  23329  hoid1i  23330  hoid1ri  23331  honegsubi  23337  hoddii  23530  lnopunilem2  23552  elunop2  23554  lnophm  23560  imaelshi  23599  cnlnadjlem8  23615  pjnmopi  23689  pjsdii  23696  pjddii  23697  pjtoi  23720  chirred  23936  cnzh  24389  rezh  24390  dmvlsiga  24547  volmeas  24622  sxbrsigalem3  24657  coinfliprv  24775  ballotlem7  24828  kur14lem9  24935  prodf1f  25255  dfon2lem7  25451  epsetlike  25504  wfisg  25519  frinsg  25555  wfr3  25591  tfrALTlem  25592  bdayfo  25665  nodense  25679  fobigcup  25780  axcontlem2  25939  onsucsuccmpi  26228  heicant  26281  mblfinlem1  26283  volsupnfl  26291  dvtan  26297  itg2addnc  26301  nn0prpwlem  26367  refref  26407  topmeet  26435  indexa  26477  sstotbnd2  26525  heiborlem7  26568  mzpclall  26896  dgraaf  27441  phisum  27607  stoweidlem57  27894  wallispilem3  27904  stirlinglem13  27923  bnj580  29458  bnj1384  29575  bnj1497  29603  isatliN  30274  atpsubN  30724  idldil  31085  cdleme50ldil  31519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179  df-ral 2717
  Copyright terms: Public domain W3C validator