Theorem rgen 3056

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 3055	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		rgen.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	mpgbir 1806	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3054

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

This theorem depends on definitions:  df-bi 208  df-ral 3055

This theorem is referenced by:  ralel  3057  rgenw  3058  mprg  3060  mprgbir  3061  nrex  3068  rgen2  3180  r19.21be  3233  rexlimi  3240  rgen2a  3336  sbcth2  3823  unimax  4882  reusv2lem4  5337  fnopab  6630  fmpti  7060  sorpssuni  7682  sorpssint  7683  onssmin  7742  tfis  7802  omssnlim  7828  finds  7843  finds2  7845  opabex3  7916  seqomlem2  8387  findcard3  9190  fifo  9342  fisupcl  9380  dfom3  9566  cantnfvalf  9584  frinsg  9673  rankf  9716  scottex  9807  cplem1  9811  harcard  9900  cardiun  9904  r0weon  9932  acnnum  9972  alephon  9989  alephsmo  10022  alephf1ALT  10023  alephfplem4  10027  dfac5lem4  10046  dfac5lem4OLD  10048  dfacacn  10062  kmlem1  10071  cflem  10165  cflemOLD  10166  cflecard  10173  cfsmolem  10190  fin23lem17  10258  hsmexlem4  10349  omina  10612  0tsk  10676  inar1  10696  wfgru  10737  reclem2pr  10969  nnssre  12176  nnsscn  12177  dfnn2  12185  dfnn3  12186  nnind  12190  nnsub  12219  dfuzi  12618  uzsupss  12888  cnref1o  12933  xrsupsslem  13257  xrinfmsslem  13258  xrsup0  13273  reltre  13291  rpltrp  13292  reltxrnmnf  13293  seqexw  13977  ser0f  14015  bccl  14282  hashkf  14292  hashbc  14413  wrdind  14682  01sqrexlem5  15206  sqrtf  15324  ackbijnn  15791  incexclem  15799  prodf1f  15855  eff2  16064  reeff1  16085  sqrt2irr  16214  prmind2  16652  3prm  16661  phisum  16759  pockthi  16876  infpn2  16882  prminf  16884  prmreclem2  16886  prmrec  16891  1arith  16896  1arith2  16897  vdwlem13  16962  ramz  16994  prmgap  17028  prmgaplcm  17029  prmgapprmo  17031  prmlem1a  17075  xpsff1o  17529  isacs1i  17621  dmaf  18014  cdaf  18015  coapm  18036  lublecllem  18322  chninf  18599  ex-chn1  18601  ex-chn2  18602  smndex1mnd  18879  pwmnd  18906  pmtrdifel  19453  pmtrdifwrdel  19458  odf  19510  efgrelexlemb  19723  dprd2da  20017  rngmgpf  20136  mgpf  20227  prdscrngd  20299  crhmsubc  20661  drhmsubc  20760  drngcat  20761  fldcat  20762  fldhmsubc  20764  cnfld1  21379  cnsubglem  21398  cnmsubglem  21412  nn0srg  21419  rge0srg  21420  pzriprnglem4  21466  pzriprnglem9  21471  pzriprnglem14  21476  pmatcoe1fsupp  22691  isbasis3g  22939  basdif0  22943  distop  22985  mretopd  23082  2ndcsep  23449  refref  23503  kqf  23737  fbssfi  23827  filconn  23873  prdstmdd  24114  ustfilxp  24203  prdsxmslem2  24519  qdensere  24759  recld2  24805  isclmi0  25090  iscvsi  25121  ovolf  25474  dyadmax  25590  dveflem  25971  mdegxrf  26058  fta1  26299  vieta1  26303  aalioulem2  26324  taylfval  26349  pilem2  26442  pilem3  26443  recosf1o  26524  divlogrlim  26624  logcn  26636  ressatans  26923  leibpi  26931  ftalem3  27063  chtub  27200  2sqlem6  27411  2sqlem10  27416  2sqreulem4  27442  chtppilim  27463  pntpbnd1  27574  pntlem3  27597  padicabvf  27619  bdayfo  27666  nodense  27681  oldf  27854  cutsfo  27922  addsfo  28000  negsf  28069  negsfo  28070  subsfo  28082  oniso  28288  dfn0s2  28349  n0subs  28380  bdayn0sf1o  28387  dfnns2  28389  zsoring  28426  bdaypw2n0bndlem  28480  bdayfinbndlem2  28485  z12zsodd  28499  axcontlem2  29059  nbgrnself  29453  vtxdginducedm1  29637  isgrpoi  30594  isvciOLD  30676  cnidOLD  30678  isnvi  30709  ipasslem8  30933  hilid  31257  hlimf  31333  shsspwh  31342  pjrni  31798  pjmf1  31812  df0op2  31848  dfiop2  31849  hoaddcomi  31868  hoaddassi  31872  hocadddiri  31875  hocsubdiri  31876  hoaddridi  31882  ho0coi  31884  hoid1i  31885  hoid1ri  31886  honegsubi  31892  hoddii  32085  lnopunilem2  32107  elunop2  32109  lnophm  32115  imaelshi  32154  cnlnadjlem8  32170  pjnmopi  32244  pjsdii  32251  pjddii  32252  pjtoi  32275  chirred  32491  nnindf  32919  nn0min  32920  wrdt2ind  33039  zringfrac  33644  ccfldsrarelvec  33862  constrconj  33936  2sqr3minply  33971  cos9thpiminply  33979  esum2d  34284  dmvlsiga  34320  volmeas  34422  ddemeas  34427  sxbrsigalem3  34463  coinfliprv  34674  ballotlem7  34727  signsw0glem  34744  rpsqrtcn  34784  tgoldbachgt  34854  bnj580  35102  bnj1384  35221  bnj1497  35249  fineqvnttrclse  35312  onvf1odlem1  35338  kur14lem9  35449  sat1el2xp  35614  msrf  35777  dfon2lem7  36022  fobigcup  36133  nn0prpwlem  36557  topmeet  36599  onsucsuccmpi  36678  dfttc4lem2  36764  taupilemrplb  37687  relowlssretop  37732  ptrecube  37994  poimirlem27  38021  heicant  38029  mblfinlem1  38031  volsupnfl  38039  dvtan  38044  itg2addnc  38048  indexa  38107  sstotbnd2  38148  heiborlem7  38191  disjimeceqim  39178  atpsubN  40252  idldil  40613  cdleme50ldil  41047  mzpclall  43183  dgraaf  43599  arearect  43667  areaquad  43668  onintunirab  43679  onsupuni  43681  infordmin  43983  omiscard  43994  clsk1indlem2  44493  clsk1indlem4  44495  mnuunid  44728  mnurndlem1  44732  prmunb2  44762  radcnvrat  44765  trwf  45410  rankrelp  45411  wfac8prim  45453  unirnmapsn  45666  ssmapsn  45668  upbdrech  45760  supminfxr  45914  supminfxr2  45919  supminfxrrnmpt  45921  rexanuz2nf  45942  fsumiunss  46027  resincncf  46325  dmvolss  46435  volioof  46437  stoweidlem57  46507  wallispilem3  46517  stirlinglem13  46536  dirkertrigeqlem3  46550  fourierdlem62  46618  salexct  46784  salexct3  46792  salgencntex  46793  salgensscntex  46794  gsumge0cl  46821  0ome  46979  icoresmbl  46993  hoidmv1le  47044  smflimlem1  47221  smfpimbor1lem2  47249  smfliminflem  47280  natlocalincr  47328  sinnpoly  47361  ralndv1  47575  fmtno4prm  48060  31prm  48082  tgoldbach  48315  gpg5grlim  48591  gpg5grlic  48592  nn0mnd  48677  2zlidl  48738  2zrngagrp  48747  2zrngnmlid  48753  crhmsubcALTV  48825  drhmsubcALTV  48827  drngcatALTV  48828  fldcatALTV  48829  fldhmsubcALTV  48831  zlmodzxznm  48995  ldepsnlinc  49006  nn0sumshdiglem2  49120  itcovalpclem1  49168  itcovalt2lem1  49173  rrx2xpref1o  49216  slotresfo  49396  basresposfo  49475  oppff1  49645  setc2othin  49963  setcsnterm  49987  onsetrec  50205