Theorem rgenw 3049

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

Syntax hints:   ∈ wcel 2109  ∀wral 3045

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 3046

This theorem is referenced by:  rgen2w  3050  reuss  4293  reuun1  4294  rabnc  4357  riinrab  5051  0disj  5103  iinexg  5306  epse  5623  xpiindi  5802  eliunxp  5804  opeliunxp2  5805  elrnmpti  5929  cnviin  6262  fnmpti  6664  eqfnfv  7006  eufnfv  7206  mpoeq12  7465  porpss  7706  iunex  7950  abrexex2  7951  mpoex  8061  suppssov1  8179  suppssov2  8180  suppssfv  8184  opeliunxp2f  8192  onnseq  8316  ixpssmap  8908  boxcutc  8917  nneneq  9176  finsschain  9317  dfom3  9607  cantnfdm  9624  rankuni2b  9813  rankval4  9827  alephf1  10045  dfac4  10082  dfacacn  10102  infmap2  10177  cfeq0  10216  fin23lem28  10300  axdc2lem  10408  axcclem  10417  ac6  10440  iundom  10502  konigthlem  10528  iunctb  10534  tskmid  10800  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  uzf  12803  seqof  14031  hashbclem  14424  rlimclim1  15518  fsumcom2  15747  ackbijnn  15801  fprodcom2  15957  lcmf0  16611  phisum  16768  sumhash  16874  ramcl  17007  prdsvallem  17424  prdsval  17425  prdsbas  17427  prdshom  17437  imasplusg  17487  imasmulr  17488  imasvsca  17490  imasip  17491  imasaddfnlem  17498  imasvscafn  17507  isfunc  17833  wunfunc  17870  isnat  17919  natffn  17921  wunnat  17928  fucsect  17944  setcepi  18057  grpinvfval  18917  odfval  19469  dfod2  19501  ghmcyg  19833  gsum2d2lem  19910  gsum2d2  19911  gsumcom2  19912  dmdprd  19937  dprdval  19942  dprdf11  19962  dprd2d2  19983  dpjeq  19998  pgpfac1lem2  20014  pgpfac1lem3  20016  pgpfac1lem4  20017  mptscmfsupp0  20840  00lsp  20894  ocv0  21593  ofco2  22345  tgidm  22874  pptbas  22902  tgrest  23053  iscnp2  23133  ist1-3  23243  discmp  23292  1stcfb  23339  lly1stc  23390  disllycmp  23392  dis1stc  23393  comppfsc  23426  txbas  23461  ptbasfi  23475  ptpjopn  23506  dfac14  23512  ptrescn  23533  xkoptsub  23548  fclsval  23902  ptcmplem2  23947  ptcmplem3  23948  cnextrel  23957  tsmsfbas  24022  ustuqtop  24141  prdsxmetlem  24263  ressprdsds  24266  prdsxmslem2  24424  zcld  24709  xrge0tsms  24730  metdsf  24744  metdsge  24745  minveclem1  25331  minveclem3b  25335  minveclem6  25341  uniioombllem4  25494  uniioombllem6  25496  ismbf3d  25562  i1f1lem  25597  reldv  25778  ellimc2  25785  limcflf  25789  limciun  25802  dvfval  25805  dvrec  25866  dvlipcn  25906  mdegle0  25989  ply1nzb  26035  quotlem  26215  taylfval  26273  ulmdvlem1  26316  ulmdvlem2  26317  ulmdvlem3  26318  psercn  26343  sqff1o  27099  lgsquadlem2  27299  disjxwwlksn  29841  disjxwwlkn  29850  numclwwlk3lem2  30320  grpoidval  30449  grpoidinv2  30451  grpoinv  30461  minvecolem1  30810  minvecolem5  30817  minvecolem6  30818  adjbdln  32019  dfcnv2  32607  intimafv  32641  rexdiv  32853  gsumpart  33004  xrge0tsmsd  33009  fedgmullem2  33633  irngval  33687  rspectopn  33864  zarcls  33871  zartopn  33872  esumnul  34045  esum0  34046  hasheuni  34082  esum2d  34090  ldgenpisyslem3  34162  measvuni  34211  measdivcstALTV  34222  ddemeas  34233  carsgclctunlem2  34317  eulerpartlemgs2  34378  probfinmeasbALTV  34427  0rrv  34449  signsplypnf  34548  signsply0  34549  hgt750lemb  34654  bnj226  34731  bnj98  34864  bnj517  34882  bnj893  34925  bnj1137  34992  subfacf  35169  subfacp1lem6  35179  cvmsss2  35268  cvmliftlem1  35279  ixpeq12i  36196  bj-rabtr  36925  relowlssretop  37358  fin2so  37608  matunitlindflem1  37617  ptrest  37620  poimirlem23  37644  poimirlem24  37645  poimirlem27  37648  poimirlem30  37651  poimirlem32  37653  cnambfre  37669  upixp  37730  0totbnd  37774  prdsbnd  37794  prdstotbnd  37795  cntotbnd  37797  rrnequiv  37836  ac6s6  38173  cdlemefrs32fva  40401  cdlemkid5  40936  cdlemk56  40972  dihf11lem  41267  addinvcom  42427  0dioph  42773  vdioph  42774  rmxyelqirrOLD  42906  pw2f1ocnv  43033  pwinfi  43560  eliunov2  43675  fvmptiunrelexplb0d  43680  fvmptiunrelexplb1d  43682  iunrelexp0  43698  ntrrn  44118  dssmapntrcls  44124  mnurndlem1  44277  rankrelp  44957  0elaxnul  44980  prclaxpr  44982  uniclaxun  44983  omssaxinf2  44985  wessf1ornlem  45186  axccdom  45223  fnmptif  45266  fsumiunss  45580  limcdm0  45623  liminfval2  45773  liminflelimsuplem  45780  cnrefiisplem  45834  0cnf  45882  dvsinax  45918  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem3  45953  iblempty  45970  fourierdlem89  46200  fourierdlem91  46202  fourierdlem100  46211  fourierdlem108  46219  fourierdlem112  46223  salexct3  46347  salgensscntex  46349  omeiunle  46522  0ome  46534  hoissrrn  46554  ovn0  46571  hoissrrn2  46583  hspmbl  46634  ovolval5lem2  46658  iunhoiioolem  46680  vonioolem2  46686  vonicclem2  46689  smflimlem1  46776  smfsuplem1  46816  smfinflem  46822  smflimsuplem1  46825  smflimsuplem2  46826  smflimsuplem3  46827  smflimsuplem4  46828  smflimsuplem5  46829  smflimsuplem7  46831  smfliminflem  46835  ralndv2  47111  iccelpart  47438  eliunxp2  48326  1arymaptf1  48635  iinxp  48823  iinfssclem2  49048  iinfssclem3  49049  iinfssc  49050  imasubclem1  49097