Theorem rgen 3054

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

Step	Hyp	Ref	Expression
1		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		rgen.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	mpgbir 1801	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  ralel  3055  rgenw  3056  mprg  3058  mprgbir  3059  nrex  3065  rgen2  3177  r19.21be  3230  rexlimi  3237  rgen2a  3342  sbcth2  3835  unimax  4901  reusv2lem4  5347  fnopab  6631  fmpti  7059  sorpssuni  7679  sorpssint  7680  onssmin  7739  tfis  7799  omssnlim  7825  finds  7840  finds2  7842  opabex3  7913  seqomlem2  8384  findcard3  9187  fifo  9339  fisupcl  9377  dfom3  9560  cantnfvalf  9578  frinsg  9667  rankf  9710  scottex  9801  cplem1  9805  harcard  9894  cardiun  9898  r0weon  9926  acnnum  9966  alephon  9983  alephsmo  10016  alephf1ALT  10017  alephfplem4  10021  dfac5lem4  10040  dfac5lem4OLD  10042  dfacacn  10056  kmlem1  10065  cflem  10159  cflemOLD  10160  cflecard  10167  cfsmolem  10184  fin23lem17  10252  hsmexlem4  10343  omina  10606  0tsk  10670  inar1  10690  wfgru  10731  reclem2pr  10963  nnssre  12153  nnsscn  12154  dfnn2  12162  dfnn3  12163  nnind  12167  nnsub  12193  dfuzi  12587  uzsupss  12857  cnref1o  12902  xrsupsslem  13226  xrinfmsslem  13227  xrsup0  13242  reltre  13260  rpltrp  13261  reltxrnmnf  13262  seqexw  13944  ser0f  13982  bccl  14249  hashkf  14259  hashbc  14380  wrdind  14649  01sqrexlem5  15173  sqrtf  15291  ackbijnn  15755  incexclem  15763  prodf1f  15819  eff2  16028  reeff1  16049  sqrt2irr  16178  prmind2  16616  3prm  16625  phisum  16722  pockthi  16839  infpn2  16845  prminf  16847  prmreclem2  16849  prmrec  16854  1arith  16859  1arith2  16860  vdwlem13  16925  ramz  16957  prmgap  16991  prmgaplcm  16992  prmgapprmo  16994  prmlem1a  17038  xpsff1o  17492  isacs1i  17584  dmaf  17977  cdaf  17978  coapm  17999  lublecllem  18285  chninf  18562  ex-chn1  18564  ex-chn2  18565  smndex1mnd  18839  pwmnd  18866  pmtrdifel  19413  pmtrdifwrdel  19418  odf  19470  efgrelexlemb  19683  dprd2da  19977  rngmgpf  20096  mgpf  20187  prdscrngd  20261  crhmsubc  20619  drhmsubc  20718  drngcat  20719  fldcat  20720  fldhmsubc  20722  cnfld1  21352  cnfld1OLD  21353  cnsubglem  21374  cnmsubglem  21389  nn0srg  21396  rge0srg  21397  pzriprnglem4  21443  pzriprnglem9  21448  pzriprnglem14  21453  pmatcoe1fsupp  22649  isbasis3g  22897  basdif0  22901  distop  22943  mretopd  23040  2ndcsep  23407  refref  23461  kqf  23695  fbssfi  23785  filconn  23831  prdstmdd  24072  ustfilxp  24161  prdsxmslem2  24477  qdensere  24717  recld2  24763  isclmi0  25058  iscvsi  25089  ovolf  25443  dyadmax  25559  dveflem  25943  mdegxrf  26033  fta1  26276  vieta1  26280  aalioulem2  26301  taylfval  26326  pilem2  26422  pilem3  26423  recosf1o  26504  divlogrlim  26604  logcn  26616  ressatans  26904  leibpi  26912  ftalem3  27045  chtub  27183  2sqlem6  27394  2sqlem10  27399  2sqreulem4  27425  chtppilim  27446  pntpbnd1  27557  pntlem3  27580  padicabvf  27602  bdayfo  27649  nodense  27664  oldf  27835  scutfo  27887  addsfo  27965  negsf  28034  negsfo  28035  subsfo  28047  onsiso  28252  dfn0s2  28312  n0subs  28342  bdayn0sf1o  28349  dfnns2  28351  zsoring  28388  bdaypw2n0sbndlem  28442  bdayfinbndlem2  28447  zs12zodd  28461  axcontlem2  29021  nbgrnself  29415  vtxdginducedm1  29600  isgrpoi  30556  isvciOLD  30638  cnidOLD  30640  isnvi  30671  ipasslem8  30895  hilid  31219  hlimf  31295  shsspwh  31304  pjrni  31760  pjmf1  31774  df0op2  31810  dfiop2  31811  hoaddcomi  31830  hoaddassi  31834  hocadddiri  31837  hocsubdiri  31838  hoaddridi  31844  ho0coi  31846  hoid1i  31847  hoid1ri  31848  honegsubi  31854  hoddii  32047  lnopunilem2  32069  elunop2  32071  lnophm  32077  imaelshi  32116  cnlnadjlem8  32132  pjnmopi  32206  pjsdii  32213  pjddii  32214  pjtoi  32237  chirred  32453  nnindf  32881  nn0min  32882  wrdt2ind  33016  zringfrac  33616  ccfldsrarelvec  33809  constrconj  33883  2sqr3minply  33918  cos9thpiminply  33926  esum2d  34231  dmvlsiga  34267  volmeas  34369  ddemeas  34374  sxbrsigalem3  34410  coinfliprv  34621  ballotlem7  34674  signsw0glem  34691  rpsqrtcn  34731  tgoldbachgt  34801  bnj580  35050  bnj1384  35169  bnj1497  35197  fineqvnttrclse  35261  onvf1odlem1  35278  kur14lem9  35389  sat1el2xp  35554  msrf  35717  dfon2lem7  35962  fobigcup  36073  nn0prpwlem  36497  topmeet  36539  onsucsuccmpi  36618  taupilemrplb  37496  relowlssretop  37539  ptrecube  37792  poimirlem27  37819  heicant  37827  mblfinlem1  37829  volsupnfl  37837  dvtan  37842  itg2addnc  37846  indexa  37905  sstotbnd2  37946  heiborlem7  37989  disjimeceqim  38976  atpsubN  40050  idldil  40411  cdleme50ldil  40845  mzpclall  43005  dgraaf  43425  arearect  43493  areaquad  43494  onintunirab  43505  onsupuni  43507  infordmin  43809  omiscard  43820  clsk1indlem2  44319  clsk1indlem4  44321  mnuunid  44554  mnurndlem1  44558  prmunb2  44588  radcnvrat  44591  trwf  45236  rankrelp  45237  wfac8prim  45279  unirnmapsn  45494  ssmapsn  45496  upbdrech  45589  supminfxr  45744  supminfxr2  45749  supminfxrrnmpt  45751  rexanuz2nf  45772  fsumiunss  45857  resincncf  46155  dmvolss  46265  volioof  46267  stoweidlem57  46337  wallispilem3  46347  stirlinglem13  46366  dirkertrigeqlem3  46380  fourierdlem62  46448  salexct  46614  salexct3  46622  salgencntex  46623  salgensscntex  46624  gsumge0cl  46651  0ome  46809  icoresmbl  46823  hoidmv1le  46874  smflimlem1  47051  smfpimbor1lem2  47079  smfliminflem  47110  natlocalincr  47156  sinnpoly  47173  ralndv1  47387  fmtno4prm  47857  31prm  47879  tgoldbach  48099  gpg5grlim  48375  gpg5grlic  48376  nn0mnd  48461  2zlidl  48522  2zrngagrp  48531  2zrngnmlid  48537  crhmsubcALTV  48609  drhmsubcALTV  48611  drngcatALTV  48612  fldcatALTV  48613  fldhmsubcALTV  48615  zlmodzxznm  48779  ldepsnlinc  48790  nn0sumshdiglem2  48904  itcovalpclem1  48952  itcovalt2lem1  48957  rrx2xpref1o  49000  slotresfo  49180  basresposfo  49259  oppff1  49429  setc2othin  49747  setcsnterm  49771  onsetrec  49989