Theorem rgen 3074

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064

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 3069

This theorem is referenced by:  ralel  3075  rgenw  3076  mprg  3078  mprgbir  3079  rgen2  3120  r19.21be  3135  rgen2a  3158  nrex  3197  rexlimiv  3209  rexlimi  3248  sbcth2  3817  r19.2zb  4426  ral0OLD  4447  unimax  4877  mpteq1OLD  5168  mpteq2iaOLD  5178  reusv2lem4  5324  wfisgOLD  6257  fnopab  6571  fmpti  6986  sorpssuni  7585  sorpssint  7586  onssmin  7642  tfis  7701  omssnlim  7727  finds  7745  finds2  7747  opabex3  7810  wfr3OLD  8169  seqomlem2  8282  findcard3  9057  fifo  9191  fisupcl  9228  dfom3  9405  cantnfvalf  9423  frinsg  9509  rankf  9552  scottex  9643  cplem1  9647  harcard  9736  cardiun  9740  r0weon  9768  acnnum  9808  alephon  9825  alephsmo  9858  alephf1ALT  9859  alephfplem4  9863  dfac5lem4  9882  dfacacn  9897  kmlem1  9906  cflem  10002  cflecard  10009  cfsmolem  10026  fin23lem17  10094  hsmexlem4  10185  omina  10447  0tsk  10511  inar1  10531  wfgru  10572  reclem2pr  10804  nnssre  11977  nnsscn  11978  dfnn2  11986  dfnn3  11987  nnind  11991  nnsub  12017  dfuzi  12411  uzsupss  12680  cnref1o  12725  xrsupsslem  13041  xrinfmsslem  13042  xrsup0  13057  reltre  13074  rpltrp  13075  reltxrnmnf  13076  seqexw  13737  ser0f  13776  bccl  14036  hashkf  14046  hashbc  14165  wrdind  14435  sqrlem5  14958  sqrtf  15075  ackbijnn  15540  incexclem  15548  prodf1f  15604  eff2  15808  reeff1  15829  sqrt2irr  15958  prmind2  16390  3prm  16399  phisum  16491  pockthi  16608  infpn2  16614  prminf  16616  prmreclem2  16618  prmrec  16623  1arith  16628  1arith2  16629  vdwlem13  16694  ramz  16726  prmgap  16760  prmgaplcm  16761  prmgapprmo  16763  prmlem1a  16808  xpsff1o  17278  isacs1i  17366  dmaf  17764  cdaf  17765  coapm  17786  lublecllem  18078  smndex1mnd  18549  pwmnd  18576  pmtrdifel  19088  pmtrdifwrdel  19093  odf  19145  efgrelexlemb  19356  dprd2da  19645  mgpf  19798  prdscrngd  19852  cnfld1  20623  cnsubglem  20647  cnmsubglem  20661  nn0srg  20668  rge0srg  20669  pmatcoe1fsupp  21850  isbasis3g  22099  basdif0  22103  distop  22145  mretopd  22243  2ndcsep  22610  refref  22664  kqf  22898  fbssfi  22988  filconn  23034  prdstmdd  23275  ustfilxp  23364  prdsxmslem2  23685  qdensere  23933  recld2  23977  isclmi0  24261  iscvsi  24292  ovolf  24646  dyadmax  24762  dveflem  25143  mdegxrf  25233  fta1  25468  vieta1  25472  aalioulem2  25493  taylfval  25518  pilem2  25611  pilem3  25612  recosf1o  25691  divlogrlim  25790  logcn  25802  ressatans  26084  leibpi  26092  ftalem3  26224  chtub  26360  2sqlem6  26571  2sqlem10  26576  2sqreulem4  26602  chtppilim  26623  pntpbnd1  26734  pntlem3  26757  padicabvf  26779  axcontlem2  27333  nbgrnself  27726  vtxdginducedm1  27910  isgrpoi  28860  isvciOLD  28942  cnidOLD  28944  isnvi  28975  ipasslem8  29199  hilid  29523  hlimf  29599  shsspwh  29608  pjrni  30064  pjmf1  30078  df0op2  30114  dfiop2  30115  hoaddcomi  30134  hoaddassi  30138  hocadddiri  30141  hocsubdiri  30142  hoaddid1i  30148  ho0coi  30150  hoid1i  30151  hoid1ri  30152  honegsubi  30158  hoddii  30351  lnopunilem2  30373  elunop2  30375  lnophm  30381  imaelshi  30420  cnlnadjlem8  30436  pjnmopi  30510  pjsdii  30517  pjddii  30518  pjtoi  30541  chirred  30757  nnindf  31133  nn0min  31134  wrdt2ind  31225  ccfldsrarelvec  31741  esum2d  32061  dmvlsiga  32097  volmeas  32199  ddemeas  32204  sxbrsigalem3  32239  coinfliprv  32449  ballotlem7  32502  signsw0glem  32532  rpsqrtcn  32573  tgoldbachgt  32643  bnj580  32893  bnj1384  33012  bnj1497  33040  kur14lem9  33176  sat1el2xp  33341  msrf  33504  dfon2lem7  33765  bdayfo  33880  nodense  33895  oldf  34041  scutfo  34084  fobigcup  34202  nn0prpwlem  34511  topmeet  34553  onsucsuccmpi  34632  taupilemrplb  35491  relowlssretop  35534  ptrecube  35777  poimirlem27  35804  heicant  35812  mblfinlem1  35814  volsupnfl  35822  dvtan  35827  itg2addnc  35831  indexa  35891  sstotbnd2  35932  heiborlem7  35975  atpsubN  37767  idldil  38128  cdleme50ldil  38562  mzpclall  40549  dgraaf  40972  arearect  41046  areaquad  41047  infordmin  41139  omiscard  41150  clsk1indlem2  41652  clsk1indlem4  41654  mnuunid  41895  mnurndlem1  41899  prmunb2  41929  radcnvrat  41932  unirnmapsn  42754  ssmapsn  42756  upbdrech  42844  supminfxr  43004  supminfxr2  43009  supminfxrrnmpt  43011  fsumiunss  43116  resincncf  43416  dmvolss  43526  volioof  43528  stoweidlem57  43598  wallispilem3  43608  stirlinglem13  43627  dirkertrigeqlem3  43641  fourierdlem62  43709  salexct  43873  salexct3  43881  salgencntex  43882  salgensscntex  43883  gsumge0cl  43909  0ome  44067  icoresmbl  44081  hoidmv1le  44132  smflimlem1  44306  smfpimbor1lem2  44333  smfliminflem  44363  ralndv1  44597  fmtno4prm  45027  31prm  45049  tgoldbach  45269  nn0mnd  45373  2zlidl  45492  2zrngagrp  45501  2zrngnmlid  45507  crhmsubc  45636  drhmsubc  45638  drngcat  45639  fldcat  45640  fldhmsubc  45642  crhmsubcALTV  45654  drhmsubcALTV  45656  drngcatALTV  45657  fldcatALTV  45658  fldhmsubcALTV  45660  zlmodzxznm  45838  ldepsnlinc  45849  nn0sumshdiglem2  45968  itcovalpclem1  46016  itcovalt2lem1  46021  rrx2xpref1o  46064  setc2othin  46337  onsetrec  46413  natlocalincr  46511