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 2113  ∀wral 3051

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 207  df-ral 3052

This theorem is referenced by:  rgen2w  3056  reuss  4279  reuun1  4280  rabnc  4343  riinrab  5039  0disj  5091  iinexg  5293  epse  5606  xpiindi  5784  eliunxp  5786  opeliunxp2  5787  elrnmpti  5911  cnviin  6244  fnmpti  6635  eqfnfv  6976  eufnfv  7175  mpoeq12  7431  porpss  7672  iunex  7912  abrexex2  7913  mpoex  8023  suppssov1  8139  suppssov2  8140  suppssfv  8144  opeliunxp2f  8152  onnseq  8276  ixpssmap  8870  boxcutc  8879  nneneq  9130  finsschain  9259  dfom3  9556  cantnfdm  9573  rankuni2b  9765  rankval4  9779  alephf1  9995  dfac4  10032  dfacacn  10052  infmap2  10127  cfeq0  10166  fin23lem28  10250  axdc2lem  10358  axcclem  10367  ac6  10390  iundom  10452  konigthlem  10479  iunctb  10485  tskmid  10751  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  supmul  12114  uzf  12754  seqof  13982  hashbclem  14375  rlimclim1  15468  fsumcom2  15697  ackbijnn  15751  fprodcom2  15907  lcmf0  16561  phisum  16718  sumhash  16824  ramcl  16957  prdsvallem  17374  prdsval  17375  prdsbas  17377  prdshom  17387  imasplusg  17438  imasmulr  17439  imasvsca  17441  imasip  17442  imasaddfnlem  17449  imasvscafn  17458  isfunc  17788  wunfunc  17825  isnat  17874  natffn  17876  wunnat  17883  fucsect  17899  setcepi  18012  grpinvfval  18908  odfval  19461  dfod2  19493  ghmcyg  19825  gsum2d2lem  19902  gsum2d2  19903  gsumcom2  19904  dmdprd  19929  dprdval  19934  dprdf11  19954  dprd2d2  19975  dpjeq  19990  pgpfac1lem2  20006  pgpfac1lem3  20008  pgpfac1lem4  20009  mptscmfsupp0  20878  00lsp  20932  ocv0  21632  ofco2  22395  tgidm  22924  pptbas  22952  tgrest  23103  iscnp2  23183  ist1-3  23293  discmp  23342  1stcfb  23389  lly1stc  23440  disllycmp  23442  dis1stc  23443  comppfsc  23476  txbas  23511  ptbasfi  23525  ptpjopn  23556  dfac14  23562  ptrescn  23583  xkoptsub  23598  fclsval  23952  ptcmplem2  23997  ptcmplem3  23998  cnextrel  24007  tsmsfbas  24072  ustuqtop  24190  prdsxmetlem  24312  ressprdsds  24315  prdsxmslem2  24473  zcld  24758  xrge0tsms  24779  metdsf  24793  metdsge  24794  minveclem1  25380  minveclem3b  25384  minveclem6  25390  uniioombllem4  25543  uniioombllem6  25545  ismbf3d  25611  i1f1lem  25646  reldv  25827  ellimc2  25834  limcflf  25838  limciun  25851  dvfval  25854  dvrec  25915  dvlipcn  25955  mdegle0  26038  ply1nzb  26084  quotlem  26264  taylfval  26322  ulmdvlem1  26365  ulmdvlem2  26366  ulmdvlem3  26367  psercn  26392  sqff1o  27148  lgsquadlem2  27348  bdayiun  27911  disjxwwlksn  29977  disjxwwlkn  29986  numclwwlk3lem2  30459  grpoidval  30588  grpoidinv2  30590  grpoinv  30600  minvecolem1  30949  minvecolem5  30956  minvecolem6  30957  adjbdln  32158  dfcnv2  32754  intimafv  32790  rexdiv  33007  gsumpart  33146  xrge0tsmsd  33155  fedgmullem2  33787  irngval  33842  rspectopn  34024  zarcls  34031  zartopn  34032  esumnul  34205  esum0  34206  hasheuni  34242  esum2d  34250  ldgenpisyslem3  34322  measvuni  34371  measdivcstALTV  34382  ddemeas  34393  carsgclctunlem2  34476  eulerpartlemgs2  34537  probfinmeasbALTV  34586  0rrv  34608  signsplypnf  34707  signsply0  34708  hgt750lemb  34813  bnj226  34890  bnj98  35023  bnj517  35041  bnj893  35084  bnj1137  35151  rankval4b  35256  rankfilimbi  35257  fineqvnttrclse  35280  tz9.1regs  35290  subfacf  35369  subfacp1lem6  35379  cvmsss2  35468  cvmliftlem1  35479  ixpeq12i  36395  bj-rabtr  37131  relowlssretop  37568  fin2so  37808  matunitlindflem1  37817  ptrest  37820  poimirlem23  37844  poimirlem24  37845  poimirlem27  37848  poimirlem30  37851  poimirlem32  37853  cnambfre  37869  upixp  37930  0totbnd  37974  prdsbnd  37994  prdstotbnd  37995  cntotbnd  37997  rrnequiv  38036  ac6s6  38373  dmsucmap  38652  cdlemefrs32fva  40670  cdlemkid5  41205  cdlemk56  41241  dihf11lem  41536  addinvcom  42697  0dioph  43030  vdioph  43031  pw2f1ocnv  43289  pwinfi  43815  eliunov2  43930  fvmptiunrelexplb0d  43935  fvmptiunrelexplb1d  43937  iunrelexp0  43953  ntrrn  44373  dssmapntrcls  44379  mnurndlem1  44532  rankrelp  45211  0elaxnul  45234  prclaxpr  45236  uniclaxun  45237  omssaxinf2  45239  wessf1ornlem  45439  axccdom  45476  fnmptif  45519  fsumiunss  45831  limcdm0  45874  liminfval2  46022  liminflelimsuplem  46029  cnrefiisplem  46083  0cnf  46131  dvsinax  46167  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  dvnprodlem3  46202  iblempty  46219  fourierdlem89  46449  fourierdlem91  46451  fourierdlem100  46460  fourierdlem108  46468  fourierdlem112  46472  salexct3  46596  salgensscntex  46598  omeiunle  46771  0ome  46783  hoissrrn  46803  ovn0  46820  hoissrrn2  46832  hspmbl  46883  ovolval5lem2  46907  iunhoiioolem  46929  vonioolem2  46935  vonicclem2  46938  smflimlem1  47025  smfsuplem1  47065  smfinflem  47071  smflimsuplem1  47074  smflimsuplem2  47075  smflimsuplem3  47076  smflimsuplem4  47077  smflimsuplem5  47078  smflimsuplem7  47080  smfliminflem  47084  nthrucw  47140  ralndv2  47362  iccelpart  47689  eliunxp2  48590  1arymaptf1  48898  iinxp  49086  iinfssclem2  49310  iinfssclem3  49311  iinfssc  49312  imasubclem1  49359