Theorem rgenw 3055

Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1	⊢ 𝜑

Assertion

Ref	Expression
rgenw	⊢ ∀𝑥 ∈ 𝐴 𝜑

Proof of Theorem rgenw

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	2	rgen 3053	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∈ wcel 2108  ∀wral 3051

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

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

This theorem is referenced by:  rgen2w  3056  reuss  4302  reuun1  4303  rabnc  4366  riinrab  5060  0disj  5112  iinexg  5318  epse  5636  xpiindi  5815  eliunxp  5817  opeliunxp2  5818  elrnmpti  5942  cnviin  6275  fnmpti  6680  eqfnfv  7020  eufnfv  7220  mpoeq12  7478  porpss  7719  iunex  7965  abrexex2  7966  mpoex  8076  suppssov1  8194  suppssov2  8195  suppssfv  8199  opeliunxp2f  8207  onnseq  8356  ixpssmap  8944  boxcutc  8953  nneneq  9218  finsschain  9369  dfom3  9659  cantnfdm  9676  rankuni2b  9865  rankval4  9879  alephf1  10097  dfac4  10134  dfacacn  10154  infmap2  10229  cfeq0  10268  fin23lem28  10352  axdc2lem  10460  axcclem  10469  ac6  10492  iundom  10554  konigthlem  10580  iunctb  10586  tskmid  10852  supaddc  12207  supadd  12208  supmul1  12209  supmullem2  12211  supmul  12212  uzf  12853  seqof  14075  hashbclem  14468  rlimclim1  15559  fsumcom2  15788  ackbijnn  15842  fprodcom2  15998  lcmf0  16651  phisum  16808  sumhash  16914  ramcl  17047  prdsvallem  17466  prdsval  17467  prdsbas  17469  prdshom  17479  imasplusg  17529  imasmulr  17530  imasvsca  17532  imasip  17533  imasaddfnlem  17540  imasvscafn  17549  isfunc  17875  wunfunc  17912  isnat  17961  natffn  17963  wunnat  17970  fucsect  17986  setcepi  18099  grpinvfval  18959  odfval  19511  dfod2  19543  ghmcyg  19875  gsum2d2lem  19952  gsum2d2  19953  gsumcom2  19954  dmdprd  19979  dprdval  19984  dprdf11  20004  dprd2d2  20025  dpjeq  20040  pgpfac1lem2  20056  pgpfac1lem3  20058  pgpfac1lem4  20059  mptscmfsupp0  20882  00lsp  20936  ocv0  21635  ofco2  22387  tgidm  22916  pptbas  22944  tgrest  23095  iscnp2  23175  ist1-3  23285  discmp  23334  1stcfb  23381  lly1stc  23432  disllycmp  23434  dis1stc  23435  comppfsc  23468  txbas  23503  ptbasfi  23517  ptpjopn  23548  dfac14  23554  ptrescn  23575  xkoptsub  23590  fclsval  23944  ptcmplem2  23989  ptcmplem3  23990  cnextrel  23999  tsmsfbas  24064  ustuqtop  24183  prdsxmetlem  24305  ressprdsds  24308  prdsxmslem2  24466  zcld  24751  xrge0tsms  24772  metdsf  24786  metdsge  24787  minveclem1  25374  minveclem3b  25378  minveclem6  25384  uniioombllem4  25537  uniioombllem6  25539  ismbf3d  25605  i1f1lem  25640  reldv  25821  ellimc2  25828  limcflf  25832  limciun  25845  dvfval  25848  dvrec  25909  dvlipcn  25949  mdegle0  26032  ply1nzb  26078  quotlem  26258  taylfval  26316  ulmdvlem1  26359  ulmdvlem2  26360  ulmdvlem3  26361  psercn  26386  sqff1o  27142  lgsquadlem2  27342  disjxwwlksn  29832  disjxwwlkn  29841  numclwwlk3lem2  30311  grpoidval  30440  grpoidinv2  30442  grpoinv  30452  minvecolem1  30801  minvecolem5  30808  minvecolem6  30809  adjbdln  32010  dfcnv2  32600  intimafv  32634  rexdiv  32846  gsumpart  32997  xrge0tsmsd  33002  fedgmullem2  33616  irngval  33672  rspectopn  33844  zarcls  33851  zartopn  33852  esumnul  34025  esum0  34026  hasheuni  34062  esum2d  34070  ldgenpisyslem3  34142  measvuni  34191  measdivcstALTV  34202  ddemeas  34213  carsgclctunlem2  34297  eulerpartlemgs2  34358  probfinmeasbALTV  34407  0rrv  34429  signsplypnf  34528  signsply0  34529  hgt750lemb  34634  bnj226  34711  bnj98  34844  bnj517  34862  bnj893  34905  bnj1137  34972  subfacf  35143  subfacp1lem6  35153  cvmsss2  35242  cvmliftlem1  35253  ixpeq12i  36165  bj-rabtr  36894  relowlssretop  37327  fin2so  37577  matunitlindflem1  37586  ptrest  37589  poimirlem23  37613  poimirlem24  37614  poimirlem27  37617  poimirlem30  37620  poimirlem32  37622  cnambfre  37638  upixp  37699  0totbnd  37743  prdsbnd  37763  prdstotbnd  37764  cntotbnd  37766  rrnequiv  37805  ac6s6  38142  cdlemefrs32fva  40365  cdlemkid5  40900  cdlemk56  40936  dihf11lem  41231  addinvcom  42421  0dioph  42748  vdioph  42749  rmxyelqirrOLD  42881  pw2f1ocnv  43008  pwinfi  43535  eliunov2  43650  fvmptiunrelexplb0d  43655  fvmptiunrelexplb1d  43657  iunrelexp0  43673  ntrrn  44093  dssmapntrcls  44099  mnurndlem1  44253  rankrelp  44933  0elaxnul  44956  prclaxpr  44958  uniclaxun  44959  omssaxinf2  44961  wessf1ornlem  45157  axccdom  45194  fnmptif  45237  fsumiunss  45552  limcdm0  45595  liminfval2  45745  liminflelimsuplem  45752  cnrefiisplem  45806  0cnf  45854  dvsinax  45890  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem3  45925  iblempty  45942  fourierdlem89  46172  fourierdlem91  46174  fourierdlem100  46183  fourierdlem108  46191  fourierdlem112  46195  salexct3  46319  salgensscntex  46321  omeiunle  46494  0ome  46506  hoissrrn  46526  ovn0  46543  hoissrrn2  46555  hspmbl  46606  ovolval5lem2  46630  iunhoiioolem  46652  vonioolem2  46658  vonicclem2  46661  smflimlem1  46748  smfsuplem1  46788  smfinflem  46794  smflimsuplem1  46797  smflimsuplem2  46798  smflimsuplem3  46799  smflimsuplem4  46800  smflimsuplem5  46801  smflimsuplem7  46803  smfliminflem  46807  ralndv2  47083  iccelpart  47395  eliunxp2  48257  1arymaptf1  48570  iinxp  48757  iinfssclem2  48970  iinfssclem3  48971  iinfssc  48972  imasubclem1  49011