Theorem rgenw 3065

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

Syntax hints:   ∈ wcel 2108  ∀wral 3061

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 3062

This theorem is referenced by:  rgen2w  3066  reuss  4327  reuun1  4328  rabnc  4391  riinrab  5084  0disj  5136  iinexg  5348  epse  5667  xpiindi  5846  eliunxp  5848  opeliunxp2  5849  elrnmpti  5973  cnviin  6306  fnmpti  6711  eqfnfv  7051  eufnfv  7249  mpoeq12  7506  porpss  7747  iunex  7993  abrexex2  7994  mpoex  8104  suppssov1  8222  suppssov2  8223  suppssfv  8227  opeliunxp2f  8235  onnseq  8384  ixpssmap  8972  boxcutc  8981  nneneq  9246  nneneqOLD  9258  finsschain  9399  dfom3  9687  cantnfdm  9704  rankuni2b  9893  rankval4  9907  alephf1  10125  dfac4  10162  dfacacn  10182  infmap2  10257  cfeq0  10296  fin23lem28  10380  axdc2lem  10488  axcclem  10497  ac6  10520  iundom  10582  konigthlem  10608  iunctb  10614  tskmid  10880  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  uzf  12881  seqof  14100  hashbclem  14491  rlimclim1  15581  fsumcom2  15810  ackbijnn  15864  fprodcom2  16020  lcmf0  16671  phisum  16828  sumhash  16934  ramcl  17067  prdsvallem  17499  prdsval  17500  prdsbas  17502  prdshom  17512  imasplusg  17562  imasmulr  17563  imasvsca  17565  imasip  17566  imasaddfnlem  17573  imasvscafn  17582  isfunc  17909  wunfunc  17946  isnat  17995  natffn  17997  wunnat  18004  fucsect  18020  setcepi  18133  grpinvfval  18996  odfval  19550  dfod2  19582  ghmcyg  19914  gsum2d2lem  19991  gsum2d2  19992  gsumcom2  19993  dmdprd  20018  dprdval  20023  dprdf11  20043  dprd2d2  20064  dpjeq  20079  pgpfac1lem2  20095  pgpfac1lem3  20097  pgpfac1lem4  20098  mptscmfsupp0  20925  00lsp  20979  ocv0  21695  ofco2  22457  tgidm  22987  pptbas  23015  tgrest  23167  iscnp2  23247  ist1-3  23357  discmp  23406  1stcfb  23453  lly1stc  23504  disllycmp  23506  dis1stc  23507  comppfsc  23540  txbas  23575  ptbasfi  23589  ptpjopn  23620  dfac14  23626  ptrescn  23647  xkoptsub  23662  fclsval  24016  ptcmplem2  24061  ptcmplem3  24062  cnextrel  24071  tsmsfbas  24136  ustuqtop  24255  prdsxmetlem  24378  ressprdsds  24381  prdsxmslem2  24542  zcld  24835  xrge0tsms  24856  metdsf  24870  metdsge  24871  minveclem1  25458  minveclem3b  25462  minveclem6  25468  uniioombllem4  25621  uniioombllem6  25623  ismbf3d  25689  i1f1lem  25724  reldv  25905  ellimc2  25912  limcflf  25916  limciun  25929  dvfval  25932  dvrec  25993  dvlipcn  26033  mdegle0  26116  ply1nzb  26162  quotlem  26342  taylfval  26400  ulmdvlem1  26443  ulmdvlem2  26444  ulmdvlem3  26445  psercn  26470  sqff1o  27225  lgsquadlem2  27425  disjxwwlksn  29924  disjxwwlkn  29933  numclwwlk3lem2  30403  grpoidval  30532  grpoidinv2  30534  grpoinv  30544  minvecolem1  30893  minvecolem5  30900  minvecolem6  30901  adjbdln  32102  dfcnv2  32686  intimafv  32720  rexdiv  32908  gsumpart  33060  xrge0tsmsd  33065  fedgmullem2  33681  irngval  33735  rspectopn  33866  zarcls  33873  zartopn  33874  esumnul  34049  esum0  34050  hasheuni  34086  esum2d  34094  ldgenpisyslem3  34166  measvuni  34215  measdivcstALTV  34226  ddemeas  34237  carsgclctunlem2  34321  eulerpartlemgs2  34382  probfinmeasbALTV  34431  0rrv  34453  signsplypnf  34565  signsply0  34566  hgt750lemb  34671  bnj226  34748  bnj98  34881  bnj517  34899  bnj893  34942  bnj1137  35009  subfacf  35180  subfacp1lem6  35190  cvmsss2  35279  cvmliftlem1  35290  ixpeq12i  36202  bj-rabtr  36931  relowlssretop  37364  fin2so  37614  matunitlindflem1  37623  ptrest  37626  poimirlem23  37650  poimirlem24  37651  poimirlem27  37654  poimirlem30  37657  poimirlem32  37659  cnambfre  37675  upixp  37736  0totbnd  37780  prdsbnd  37800  prdstotbnd  37801  cntotbnd  37803  rrnequiv  37842  ac6s6  38179  cdlemefrs32fva  40402  cdlemkid5  40937  cdlemk56  40973  dihf11lem  41268  addinvcom  42461  0dioph  42789  vdioph  42790  rmxyelqirrOLD  42922  pw2f1ocnv  43049  pwinfi  43577  eliunov2  43692  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  iunrelexp0  43715  ntrrn  44135  dssmapntrcls  44141  mnurndlem1  44300  rankrelp  44977  0elaxnul  45000  prclaxpr  45002  uniclaxun  45003  omssaxinf2  45005  wessf1ornlem  45190  axccdom  45227  mpteq1dfOLD  45242  fnmptif  45272  fsumiunss  45590  limcdm0  45633  liminfval2  45783  liminflelimsuplem  45790  cnrefiisplem  45844  0cnf  45892  dvsinax  45928  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem3  45963  iblempty  45980  fourierdlem89  46210  fourierdlem91  46212  fourierdlem100  46221  fourierdlem108  46229  fourierdlem112  46233  salexct3  46357  salgensscntex  46359  omeiunle  46532  0ome  46544  hoissrrn  46564  ovn0  46581  hoissrrn2  46593  hspmbl  46644  ovolval5lem2  46668  iunhoiioolem  46690  vonioolem2  46696  vonicclem2  46699  smflimlem1  46786  smfsuplem1  46826  smfinflem  46832  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem4  46838  smflimsuplem5  46839  smflimsuplem7  46841  smfliminflem  46845  ralndv2  47118  iccelpart  47420  eliunxp2  48250  1arymaptf1  48563