Theorem rgenw 3083

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

Syntax hints:   ∈ wcel 2143  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  rgen2w  3084  reuss  4280  reuun1  4281  rabnc  4348  riinrab  5050  0disj  5102  iinexg  5318  epse  5643  xpiindi  5821  eliunxp  5823  opeliunxp2  5824  elrnmpti  5952  cnviin  6287  fnmpti  6678  eqfnfv  7025  eufnfv  7227  mpoeq12  7483  porpss  7724  iunex  7961  abrexex2  7962  mpoex  8072  suppssov1  8189  suppssov2  8190  suppssfv  8194  opeliunxp2f  8202  onnseq  8327  ixpssmap  8926  boxcutc  8935  nneneq  9186  finsschain  9312  dfom3  9612  cantnfdm  9629  rankuni2b  9821  rankval4  9835  alephf1  10065  dfac4  10102  dfacacn  10121  infmap2  10196  cfeq0  10235  fin23lem28  10319  axdc2lem  10427  axcclem  10436  ac6  10459  iundom  10521  konigthlem  10548  iunctb  10554  tskmid  10820  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  supmul  12182  uzf  12860  seqof  14091  hashbclem  14485  rlimclim1  15592  fsumcom2  15821  ackbijnn  15878  fprodcom2  16034  lcmf0  16687  phisum  16845  sumhash  16951  ramcl  17084  prdsvallem  17502  prdsval  17503  prdsbas  17505  prdshom  17515  imasplusg  17566  imasmulr  17567  imasvsca  17569  imasip  17570  imasaddfnlem  17577  imasvscafn  17586  isfunc  17916  wunfunc  17953  isnat  18002  natffn  18004  wunnat  18011  fucsect  18027  setcepi  18140  grpinvfval  19040  odfval  19597  dfod2  19629  ghmcyg  19961  gsum2d2lem  20038  gsum2d2  20039  gsumcom2  20040  dmdprd  20065  dprdval  20070  dprdf11  20090  dprd2d2  20111  dpjeq  20126  pgpfac1lem2  20142  pgpfac1lem3  20144  pgpfac1lem4  20145  mptscmfsupp0  21048  00lsp  21102  ocv0  21827  ofco2  22608  tgidm  23137  pptbas  23165  tgrest  23316  iscnp2  23396  ist1-3  23506  discmp  23555  1stcfb  23602  lly1stc  23653  disllycmp  23655  dis1stc  23656  comppfsc  23689  txbas  23724  ptbasfi  23738  ptpjopn  23769  dfac14  23775  ptrescn  23796  xkoptsub  23811  fclsval  24165  ptcmplem2  24210  ptcmplem3  24211  cnextrel  24220  tsmsfbas  24285  ustuqtop  24403  prdsxmetlem  24525  ressprdsds  24528  prdsxmslem2  24686  zcld  24971  xrge0tsms  24992  metdsf  25006  metdsge  25007  minveclem1  25583  minveclem3b  25587  minveclem6  25593  uniioombllem4  25745  uniioombllem6  25747  ismbf3d  25813  i1f1lem  25848  reldv  26029  ellimc2  26036  limcflf  26040  limciun  26053  dvfval  26056  dvrec  26114  dvlipcn  26153  mdegle0  26234  ply1nzb  26280  quotlem  26461  taylfval  26522  ulmdvlem1  26563  ulmdvlem2  26564  ulmdvlem3  26565  psercn  26589  sqff1o  27346  lgsquadlem2  27545  bdayiun  28108  disjxwwlksn  30253  disjxwwlkn  30262  numclwwlk3lem2  30735  grpoidval  30865  grpoidinv2  30867  grpoinv  30877  minvecolem1  31226  minvecolem5  31233  minvecolem6  31234  adjbdln  32435  dfcnv2  33020  intimafv  33056  rexdiv  33245  gsumpart  33383  xrge0tsmsd  33393  fedgmullem2  34020  irngval  34075  rspectopn  34257  zarcls  34264  zartopn  34265  esumnul  34438  esum0  34439  hasheuni  34475  esum2d  34483  ldgenpisyslem3  34555  measvuni  34604  measdivcstALTV  34615  ddemeas  34626  carsgclctunlem2  34709  eulerpartlemgs2  34770  probfinmeasbALTV  34819  0rrv  34841  signsplypnf  34937  signsply0  34938  hgt750lemb  35043  bnj226  35123  bnj98  35255  bnj517  35273  bnj893  35316  bnj1137  35383  rankval4b  35493  rankfilimbi  35495  fineqvnttrclse  35537  tz9.1regs  35547  subfacf  35667  subfacp1lem6  35677  cvmsss2  35766  cvmliftlem1  35777  nmulr0  36687  ixpeq12i  36733  ttciunun  37042  bj-rabtr  37586  bj-axseprep  37731  relowlssretop  38029  fin2so  38278  matunitlindflem1  38287  ptrest  38290  poimirlem23  38314  poimirlem24  38315  poimirlem27  38318  poimirlem30  38321  poimirlem32  38323  cnambfre  38339  upixp  38400  0totbnd  38444  prdsbnd  38464  prdstotbnd  38465  cntotbnd  38467  rrnequiv  38506  ac6s6  38841  dmsucmap  39137  disjimeceqim  39473  cdlemefrs32fva  41194  cdlemkid5  41729  cdlemk56  41765  dihf11lem  42060  addinvcom  43213  0dioph  43529  vdioph  43530  pw2f1ocnv  43784  pwinfi  44310  eliunov2  44425  fvmptiunrelexplb0d  44430  fvmptiunrelexplb1d  44432  iunrelexp0  44448  ntrrn  44868  dssmapntrcls  44874  mnurndlem1  45011  rankrelp  45689  0elaxnul  45712  prclaxpr  45714  uniclaxun  45715  omssaxinf2  45717  wessf1ornlem  45923  axccdom  45958  fnmptif  46000  fsumiunss  46311  limcdm0  46354  liminfval2  46502  liminflelimsuplem  46509  cnrefiisplem  46563  0cnf  46611  dvsinax  46647  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnprodlem3  46682  iblempty  46699  fourierdlem89  46929  fourierdlem91  46931  fourierdlem100  46940  fourierdlem108  46948  fourierdlem112  46952  salexct3  47076  salgensscntex  47078  omeiunle  47251  0ome  47263  hoissrrn  47283  ovn0  47300  hoissrrn2  47312  hspmbl  47363  ovolval5lem2  47387  iunhoiioolem  47409  vonioolem2  47415  vonicclem2  47418  smflimlem1  47505  smfsuplem1  47545  smfinflem  47551  smflimsuplem1  47554  smflimsuplem2  47555  smflimsuplem3  47556  smflimsuplem4  47557  smflimsuplem5  47558  smflimsuplem7  47560  smfliminflem  47564  sqrtnnaa  47624  sqrtnzqaa  47625  ralndv2  47863  iccelpart  48202  eliunxp2  49134  1arymaptf1  49442  iinxp  49629  iinfssclem2  49853  iinfssclem3  49854  iinfssc  49855  imasubclem1  49902