Theorem rgen 3150

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

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

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

This theorem depends on definitions:  df-bi 209  df-ral 3145

This theorem is referenced by:  ralel  3151  rgenw  3152  mprg  3154  mprgbir  3155  rgen2  3205  r19.21be  3212  rgen2a  3231  nrex  3271  rexlimiv  3282  rexlimi  3317  sbcth2  3869  r19.2zb  4443  ral0  4458  unimax  4876  mpteq1  5156  mpteq2ia  5159  reusv2lem4  5304  wfisg  6185  fnopab  6488  fmpti  6878  sorpssuni  7460  sorpssint  7461  onssmin  7514  tfis  7571  omssnlim  7596  finds  7610  finds2  7612  opabex3  7670  wfr3  7977  seqomlem2  8089  findcard3  8763  fifo  8898  fisupcl  8935  dfom3  9112  cantnfvalf  9130  rankf  9225  scottex  9316  cplem1  9320  harcard  9409  cardiun  9413  r0weon  9440  acnnum  9480  alephon  9497  alephsmo  9530  alephf1ALT  9531  alephfplem4  9535  dfac5lem4  9554  dfacacn  9569  kmlem1  9578  cflem  9670  cflecard  9677  cfsmolem  9694  fin23lem17  9762  hsmexlem4  9853  omina  10115  0tsk  10179  inar1  10199  wfgru  10240  reclem2pr  10472  nnssre  11644  nnsscn  11645  dfnn2  11653  dfnn3  11654  nnind  11658  nnsub  11684  dfuzi  12076  uzsupss  12343  cnref1o  12387  xrsupsslem  12703  xrinfmsslem  12704  xrsup0  12719  reltre  12736  rpltrp  12737  reltxrnmnf  12738  seqexw  13388  ser0f  13426  bccl  13685  hashkf  13695  hashbc  13814  wrdind  14086  sqrlem5  14608  sqrtf  14725  ackbijnn  15185  incexclem  15193  prodf1f  15250  eff2  15454  reeff1  15475  sqrt2irr  15604  prmind2  16031  3prm  16040  phisum  16129  pockthi  16245  infpn2  16251  prminf  16253  prmreclem2  16255  prmrec  16260  1arith  16265  1arith2  16266  vdwlem13  16331  ramz  16363  prmgap  16397  prmgaplcm  16398  prmgapprmo  16400  prmlem1a  16442  xpsff1o  16842  isacs1i  16930  dmaf  17311  cdaf  17312  coapm  17333  lublecllem  17600  smndex1mnd  18077  pwmnd  18104  pmtrdifel  18610  pmtrdifwrdel  18615  odf  18667  efgrelexlemb  18878  dprd2da  19166  mgpf  19311  prdscrngd  19365  cnfld1  20572  cnsubglem  20596  cnmsubglem  20610  nn0srg  20617  rge0srg  20618  pmatcoe1fsupp  21311  isbasis3g  21559  basdif0  21563  distop  21605  mretopd  21702  2ndcsep  22069  refref  22123  kqf  22357  fbssfi  22447  filconn  22493  prdstmdd  22734  ustfilxp  22823  prdsxmslem2  23141  qdensere  23380  recld2  23424  isclmi0  23704  iscvsi  23735  ovolf  24085  dyadmax  24201  dveflem  24578  mdegxrf  24664  fta1  24899  vieta1  24903  aalioulem2  24924  taylfval  24949  pilem2  25042  pilem3  25043  recosf1o  25121  divlogrlim  25220  logcn  25232  ressatans  25514  leibpi  25522  ftalem3  25654  chtub  25790  2sqlem6  26001  2sqlem10  26006  2sqreulem4  26032  chtppilim  26053  pntpbnd1  26164  pntlem3  26187  padicabvf  26209  axcontlem2  26753  nbgrnself  27143  vtxdginducedm1  27327  isgrpoi  28277  isvciOLD  28359  cnidOLD  28361  isnvi  28392  ipasslem8  28616  hilid  28940  hlimf  29016  shsspwh  29025  pjrni  29481  pjmf1  29495  df0op2  29531  dfiop2  29532  hoaddcomi  29551  hoaddassi  29555  hocadddiri  29558  hocsubdiri  29559  hoaddid1i  29565  ho0coi  29567  hoid1i  29568  hoid1ri  29569  honegsubi  29575  hoddii  29768  lnopunilem2  29790  elunop2  29792  lnophm  29798  imaelshi  29837  cnlnadjlem8  29853  pjnmopi  29927  pjsdii  29934  pjddii  29935  pjtoi  29958  chirred  30174  nnindf  30537  nn0min  30538  wrdt2ind  30629  ccfldsrarelvec  31058  esum2d  31354  dmvlsiga  31390  volmeas  31492  ddemeas  31497  sxbrsigalem3  31532  coinfliprv  31742  ballotlem7  31795  signsw0glem  31825  rpsqrtcn  31866  tgoldbachgt  31936  bnj580  32187  bnj1384  32306  bnj1497  32334  kur14lem9  32463  sat1el2xp  32628  msrf  32791  dfon2lem7  33036  frinsg  33089  bdayfo  33184  nodense  33198  fobigcup  33363  nn0prpwlem  33672  topmeet  33714  onsucsuccmpi  33793  taupilemrplb  34603  relowlssretop  34646  ptrecube  34894  poimirlem27  34921  heicant  34929  mblfinlem1  34931  volsupnfl  34939  dvtan  34944  itg2addnc  34948  indexa  35010  sstotbnd2  35054  heiborlem7  35097  atpsubN  36891  idldil  37252  cdleme50ldil  37686  mzpclall  39331  dgraaf  39754  arearect  39829  areaquad  39830  infordmin  39906  clsk1indlem2  40399  clsk1indlem4  40401  mnuunid  40620  mnurndlem1  40624  prmunb2  40650  radcnvrat  40653  unirnmapsn  41484  ssmapsn  41486  upbdrech  41579  supminfxr  41747  supminfxr2  41752  supminfxrrnmpt  41754  fsumiunss  41863  resincncf  42165  dmvolss  42277  volioof  42279  stoweidlem57  42349  wallispilem3  42359  stirlinglem13  42378  dirkertrigeqlem3  42392  fourierdlem62  42460  salexct  42624  salexct3  42632  salgencntex  42633  salgensscntex  42634  gsumge0cl  42660  0ome  42818  icoresmbl  42832  hoidmv1le  42883  smflimlem1  43054  smfpimbor1lem2  43081  smfliminflem  43111  ralndv1  43311  fmtno4prm  43744  31prm  43767  tgoldbach  43989  nn0mnd  44093  2zlidl  44212  2zrngagrp  44221  2zrngnmlid  44227  crhmsubc  44356  drhmsubc  44358  drngcat  44359  fldcat  44360  fldhmsubc  44362  crhmsubcALTV  44374  drhmsubcALTV  44376  drngcatALTV  44377  fldcatALTV  44378  fldhmsubcALTV  44380  zlmodzxznm  44559  ldepsnlinc  44570  nn0sumshdiglem2  44689  rrx2xpref1o  44712  onsetrec  44817