Theorem rgenw 3066

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 3064	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∈ 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:  rgen2w  3067  reuss  4317  reuun1  4318  rabnc  4388  riinrab  5088  0disj  5141  iinexg  5342  epse  5660  xpiindi  5836  eliunxp  5838  opeliunxp2  5839  elrnmpti  5960  cnviin  6286  fnmpti  6694  eqfnfv  7033  eufnfv  7231  mpoeq12  7482  porpss  7717  iunex  7955  abrexex2  7956  mpoex  8066  suppssov1  8183  suppssfv  8187  opeliunxp2f  8195  onnseq  8344  ixpssmap  8926  boxcutc  8935  nneneq  9209  nneneqOLD  9221  finsschain  9359  dfom3  9642  cantnfdm  9659  rankuni2b  9848  rankval4  9862  alephf1  10080  dfac4  10117  dfacacn  10136  infmap2  10213  cfeq0  10251  fin23lem28  10335  axdc2lem  10443  axcclem  10452  ac6  10475  iundom  10537  konigthlem  10563  iunctb  10569  tskmid  10835  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  uzf  12825  seqof  14025  hashbclem  14411  rlimclim1  15489  fsumcom2  15720  ackbijnn  15774  fprodcom2  15928  lcmf0  16571  phisum  16723  sumhash  16829  ramcl  16962  prdsvallem  17400  prdsval  17401  prdsbas  17403  prdshom  17413  imasplusg  17463  imasmulr  17464  imasvsca  17466  imasip  17467  imasaddfnlem  17474  imasvscafn  17483  isfunc  17814  wunfunc  17849  wunfuncOLD  17850  isnat  17898  natffn  17900  wunnat  17907  wunnatOLD  17908  fucsect  17925  setcepi  18038  grpinvfval  18863  odfval  19400  dfod2  19432  ghmcyg  19764  gsum2d2lem  19841  gsum2d2  19842  gsumcom2  19843  dmdprd  19868  dprdval  19873  dprdf11  19893  dprd2d2  19914  dpjeq  19929  pgpfac1lem2  19945  pgpfac1lem3  19947  pgpfac1lem4  19948  mptscmfsupp0  20537  00lsp  20592  ocv0  21230  ofco2  21953  tgidm  22483  pptbas  22511  tgrest  22663  iscnp2  22743  ist1-3  22853  discmp  22902  1stcfb  22949  lly1stc  23000  disllycmp  23002  dis1stc  23003  comppfsc  23036  txbas  23071  ptbasfi  23085  ptpjopn  23116  dfac14  23122  ptrescn  23143  xkoptsub  23158  fclsval  23512  ptcmplem2  23557  ptcmplem3  23558  cnextrel  23567  tsmsfbas  23632  ustuqtop  23751  prdsxmetlem  23874  ressprdsds  23877  prdsxmslem2  24038  zcld  24329  xrge0tsms  24350  metdsf  24364  metdsge  24365  minveclem1  24941  minveclem3b  24945  minveclem6  24951  uniioombllem4  25103  uniioombllem6  25105  ismbf3d  25171  i1f1lem  25206  reldv  25387  ellimc2  25394  limcflf  25398  limciun  25411  dvfval  25414  dvrec  25472  dvlipcn  25511  mdegle0  25595  ply1nzb  25640  quotlem  25813  taylfval  25871  ulmdvlem1  25912  ulmdvlem2  25913  ulmdvlem3  25914  psercn  25938  sqff1o  26686  lgsquadlem2  26884  disjxwwlksn  29158  disjxwwlkn  29167  numclwwlk3lem2  29637  grpoidval  29766  grpoidinv2  29768  grpoinv  29778  minvecolem1  30127  minvecolem5  30134  minvecolem6  30135  adjbdln  31336  dfcnv2  31901  intimafv  31932  rexdiv  32092  gsumpart  32207  xrge0tsmsd  32209  fedgmullem2  32715  irngval  32749  rspectopn  32847  zarcls  32854  zartopn  32855  esumnul  33046  esum0  33047  hasheuni  33083  esum2d  33091  ldgenpisyslem3  33163  measvuni  33212  measdivcstALTV  33223  ddemeas  33234  carsgclctunlem2  33318  eulerpartlemgs2  33379  probfinmeasbALTV  33428  0rrv  33450  signsplypnf  33561  signsply0  33562  hgt750lemb  33668  bnj226  33745  bnj98  33878  bnj517  33896  bnj893  33939  bnj1137  34006  subfacf  34166  subfacp1lem6  34176  cvmsss2  34265  cvmliftlem1  34276  bj-rabtr  35810  relowlssretop  36244  fin2so  36475  matunitlindflem1  36484  ptrest  36487  poimirlem23  36511  poimirlem24  36512  poimirlem27  36515  poimirlem30  36518  poimirlem32  36520  cnambfre  36536  upixp  36597  0totbnd  36641  prdsbnd  36661  prdstotbnd  36662  cntotbnd  36664  rrnequiv  36703  ac6s6  37040  cdlemefrs32fva  39271  cdlemkid5  39806  cdlemk56  39842  dihf11lem  40137  addinvcom  41304  0dioph  41516  vdioph  41517  rmxyelqirrOLD  41649  pw2f1ocnv  41776  pwinfi  42315  eliunov2  42430  fvmptiunrelexplb0d  42435  fvmptiunrelexplb1d  42437  iunrelexp0  42453  ntrrn  42873  dssmapntrcls  42879  mnurndlem1  43040  wessf1ornlem  43882  axccdom  43921  mpteq1dfOLD  43939  fnmptif  43970  fsumiunss  44291  limcdm0  44334  liminfval2  44484  liminflelimsuplem  44491  cnrefiisplem  44545  0cnf  44593  dvsinax  44629  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem3  44664  iblempty  44681  fourierdlem89  44911  fourierdlem91  44913  fourierdlem100  44922  fourierdlem108  44930  fourierdlem112  44934  salexct3  45058  salgensscntex  45060  omeiunle  45233  0ome  45245  hoissrrn  45265  ovn0  45282  hoissrrn2  45294  hspmbl  45345  ovolval5lem2  45369  iunhoiioolem  45391  vonioolem2  45397  vonicclem2  45400  smflimlem1  45487  smfsuplem1  45527  smfinflem  45533  smflimsuplem1  45536  smflimsuplem2  45537  smflimsuplem3  45538  smflimsuplem4  45539  smflimsuplem5  45540  smflimsuplem7  45542  smfliminflem  45546  ralndv2  45814  iccelpart  46101  eliunxp2  47009  1arymaptf1  47328