Theorem rgen 3064

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralel  3065  rgenw  3066  mprg  3068  mprgbir  3069  nrex  3075  rexlimivOLD  3185  rgen2  3198  r19.21be  3250  rexlimi  3257  rgen2a  3368  sbcth2  3878  r19.2zb  4495  ral0OLD  4516  unimax  4948  mpteq1OLD  5242  mpteq2iaOLD  5252  reusv2lem4  5399  wfisgOLD  6353  fnopab  6686  fmpti  7109  sorpssuni  7719  sorpssint  7720  onssmin  7777  tfis  7841  omssnlim  7867  finds  7886  finds2  7888  opabex3  7951  wfr3OLD  8335  seqomlem2  8448  findcard3  9282  findcard3OLD  9283  fifo  9424  fisupcl  9461  dfom3  9639  cantnfvalf  9657  frinsg  9743  rankf  9786  scottex  9877  cplem1  9881  harcard  9970  cardiun  9974  r0weon  10004  acnnum  10044  alephon  10061  alephsmo  10094  alephf1ALT  10095  alephfplem4  10099  dfac5lem4  10118  dfacacn  10133  kmlem1  10142  cflem  10238  cflecard  10245  cfsmolem  10262  fin23lem17  10330  hsmexlem4  10421  omina  10683  0tsk  10747  inar1  10767  wfgru  10808  reclem2pr  11040  nnssre  12213  nnsscn  12214  dfnn2  12222  dfnn3  12223  nnind  12227  nnsub  12253  dfuzi  12650  uzsupss  12921  cnref1o  12966  xrsupsslem  13283  xrinfmsslem  13284  xrsup0  13299  reltre  13316  rpltrp  13317  reltxrnmnf  13318  seqexw  13979  ser0f  14018  bccl  14279  hashkf  14289  hashbc  14409  wrdind  14669  01sqrexlem5  15190  sqrtf  15307  ackbijnn  15771  incexclem  15779  prodf1f  15835  eff2  16039  reeff1  16060  sqrt2irr  16189  prmind2  16619  3prm  16628  phisum  16720  pockthi  16837  infpn2  16843  prminf  16845  prmreclem2  16847  prmrec  16852  1arith  16857  1arith2  16858  vdwlem13  16923  ramz  16955  prmgap  16989  prmgaplcm  16990  prmgapprmo  16992  prmlem1a  17037  xpsff1o  17510  isacs1i  17598  dmaf  17996  cdaf  17997  coapm  18018  lublecllem  18310  smndex1mnd  18788  pwmnd  18815  pmtrdifel  19343  pmtrdifwrdel  19348  odf  19400  efgrelexlemb  19613  dprd2da  19907  mgpf  20065  prdscrngd  20129  cnfld1  20963  cnsubglem  20987  cnmsubglem  21001  nn0srg  21008  rge0srg  21009  pmatcoe1fsupp  22195  isbasis3g  22444  basdif0  22448  distop  22490  mretopd  22588  2ndcsep  22955  refref  23009  kqf  23243  fbssfi  23333  filconn  23379  prdstmdd  23620  ustfilxp  23709  prdsxmslem2  24030  qdensere  24278  recld2  24322  isclmi0  24606  iscvsi  24637  ovolf  24991  dyadmax  25107  dveflem  25488  mdegxrf  25578  fta1  25813  vieta1  25817  aalioulem2  25838  taylfval  25863  pilem2  25956  pilem3  25957  recosf1o  26036  divlogrlim  26135  logcn  26147  ressatans  26429  leibpi  26437  ftalem3  26569  chtub  26705  2sqlem6  26916  2sqlem10  26921  2sqreulem4  26947  chtppilim  26968  pntpbnd1  27079  pntlem3  27102  padicabvf  27124  bdayfo  27170  nodense  27185  oldf  27342  scutfo  27388  addsfo  27457  negsf  27516  negsfo  27517  axcontlem2  28213  nbgrnself  28606  vtxdginducedm1  28790  isgrpoi  29739  isvciOLD  29821  cnidOLD  29823  isnvi  29854  ipasslem8  30078  hilid  30402  hlimf  30478  shsspwh  30487  pjrni  30943  pjmf1  30957  df0op2  30993  dfiop2  30994  hoaddcomi  31013  hoaddassi  31017  hocadddiri  31020  hocsubdiri  31021  hoaddridi  31027  ho0coi  31029  hoid1i  31030  hoid1ri  31031  honegsubi  31037  hoddii  31230  lnopunilem2  31252  elunop2  31254  lnophm  31260  imaelshi  31299  cnlnadjlem8  31315  pjnmopi  31389  pjsdii  31396  pjddii  31397  pjtoi  31420  chirred  31636  nnindf  32013  nn0min  32014  wrdt2ind  32105  ccfldsrarelvec  32734  esum2d  33080  dmvlsiga  33116  volmeas  33218  ddemeas  33223  sxbrsigalem3  33260  coinfliprv  33470  ballotlem7  33523  signsw0glem  33553  rpsqrtcn  33594  tgoldbachgt  33664  bnj580  33913  bnj1384  34032  bnj1497  34060  kur14lem9  34194  sat1el2xp  34359  msrf  34522  dfon2lem7  34750  fobigcup  34861  nn0prpwlem  35196  topmeet  35238  onsucsuccmpi  35317  taupilemrplb  36190  relowlssretop  36233  ptrecube  36477  poimirlem27  36504  heicant  36512  mblfinlem1  36514  volsupnfl  36522  dvtan  36527  itg2addnc  36531  indexa  36590  sstotbnd2  36631  heiborlem7  36674  atpsubN  38613  idldil  38974  cdleme50ldil  39408  mzpclall  41451  dgraaf  41875  arearect  41950  areaquad  41951  onintunirab  41962  onsupuni  41964  infordmin  42269  omiscard  42280  clsk1indlem2  42779  clsk1indlem4  42781  mnuunid  43022  mnurndlem1  43026  prmunb2  43056  radcnvrat  43059  unirnmapsn  43899  ssmapsn  43901  upbdrech  44002  supminfxr  44161  supminfxr2  44166  supminfxrrnmpt  44168  rexanuz2nf  44190  fsumiunss  44278  resincncf  44578  dmvolss  44688  volioof  44690  stoweidlem57  44760  wallispilem3  44770  stirlinglem13  44789  dirkertrigeqlem3  44803  fourierdlem62  44871  salexct  45037  salexct3  45045  salgencntex  45046  salgensscntex  45047  gsumge0cl  45074  0ome  45232  icoresmbl  45246  hoidmv1le  45297  smflimlem1  45474  smfpimbor1lem2  45502  smfliminflem  45533  natlocalincr  45577  ralndv1  45800  fmtno4prm  46230  31prm  46252  tgoldbach  46472  nn0mnd  46576  rngmgpf  46640  2zlidl  46786  2zrngagrp  46795  2zrngnmlid  46801  crhmsubc  46930  drhmsubc  46932  drngcat  46933  fldcat  46934  fldhmsubc  46936  crhmsubcALTV  46948  drhmsubcALTV  46950  drngcatALTV  46951  fldcatALTV  46952  fldhmsubcALTV  46954  zlmodzxznm  47132  ldepsnlinc  47143  nn0sumshdiglem2  47262  itcovalpclem1  47310  itcovalt2lem1  47315  rrx2xpref1o  47358  setc2othin  47630  onsetrec  47707