Theorem rgenw 3089

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

Syntax hints:   ∈ wcel 2149  ∀wral 3085

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

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

This theorem is referenced by:  rgen2w  3090  reuss  4288  reuun1  4289  rabnc  4355  riinrab  5054  0disj  5106  iinexg  5319  epse  5644  xpiindi  5822  eliunxp  5824  opeliunxp2  5825  elrnmpti  5953  cnviin  6288  fnmpti  6679  eqfnfv  7026  eufnfv  7228  mpoeq12  7484  porpss  7725  iunex  7965  abrexex2  7966  mpoex  8076  suppssov1  8193  suppssov2  8194  suppssfv  8198  opeliunxp2f  8206  onnseq  8331  ixpssmap  8930  boxcutc  8939  nneneq  9190  finsschain  9316  dfom3  9616  cantnfdm  9633  rankuni2b  9825  rankval4  9839  alephf1  10069  dfac4  10106  dfacacn  10125  infmap2  10200  cfeq0  10240  fin23lem28  10324  axdc2lem  10432  axcclem  10441  ac6  10464  iundom  10526  konigthlem  10553  iunctb  10559  tskmid  10825  supaddc  12182  supadd  12183  supmul1  12184  supmullem2  12186  supmul  12187  uzf  12865  seqof  14095  hashbclem  14489  rlimclim1  15596  fsumcom2  15825  ackbijnn  15882  fprodcom2  16038  lcmf0  16692  phisum  16850  sumhash  16956  ramcl  17089  prdsvallem  17507  prdsval  17508  prdsbas  17510  prdshom  17520  imasplusg  17571  imasmulr  17572  imasvsca  17574  imasip  17575  imasaddfnlem  17582  imasvscafn  17591  isfunc  17921  wunfunc  17958  isnat  18007  natffn  18009  wunnat  18016  fucsect  18032  setcepi  18145  grpinvfval  19045  odfval  19602  dfod2  19634  ghmcyg  19966  gsum2d2lem  20043  gsum2d2  20044  gsumcom2  20045  dmdprd  20070  dprdval  20075  dprdf11  20095  dprd2d2  20116  dpjeq  20131  pgpfac1lem2  20147  pgpfac1lem3  20149  pgpfac1lem4  20150  mptscmfsupp0  21026  00lsp  21080  ocv0  21796  ofco2  22577  tgidm  23106  pptbas  23134  tgrest  23285  iscnp2  23365  ist1-3  23475  discmp  23524  1stcfb  23571  lly1stc  23622  disllycmp  23624  dis1stc  23625  comppfsc  23658  txbas  23693  ptbasfi  23707  ptpjopn  23738  dfac14  23744  ptrescn  23765  xkoptsub  23780  fclsval  24134  ptcmplem2  24179  ptcmplem3  24180  cnextrel  24189  tsmsfbas  24254  ustuqtop  24372  prdsxmetlem  24494  ressprdsds  24497  prdsxmslem2  24655  zcld  24940  xrge0tsms  24961  metdsf  24975  metdsge  24976  minveclem1  25552  minveclem3b  25556  minveclem6  25562  uniioombllem4  25714  uniioombllem6  25716  ismbf3d  25782  i1f1lem  25817  reldv  25998  ellimc2  26005  limcflf  26009  limciun  26022  dvfval  26025  dvrec  26083  dvlipcn  26122  mdegle0  26203  ply1nzb  26249  quotlem  26430  taylfval  26488  ulmdvlem1  26529  ulmdvlem2  26530  ulmdvlem3  26531  psercn  26555  sqff1o  27312  lgsquadlem2  27511  bdayiun  28074  disjxwwlksn  30194  disjxwwlkn  30203  numclwwlk3lem2  30676  grpoidval  30806  grpoidinv2  30808  grpoinv  30818  minvecolem1  31167  minvecolem5  31174  minvecolem6  31175  adjbdln  32376  dfcnv2  32961  intimafv  32997  rexdiv  33186  gsumpart  33324  xrge0tsmsd  33334  fedgmullem2  33965  irngval  34020  rspectopn  34202  zarcls  34209  zartopn  34210  esumnul  34383  esum0  34384  hasheuni  34420  esum2d  34428  ldgenpisyslem3  34500  measvuni  34549  measdivcstALTV  34560  ddemeas  34571  carsgclctunlem2  34654  eulerpartlemgs2  34715  probfinmeasbALTV  34764  0rrv  34786  signsplypnf  34882  signsply0  34883  hgt750lemb  34988  bnj226  35068  bnj98  35200  bnj517  35218  bnj893  35261  bnj1137  35328  rankval4b  35436  rankfilimbi  35437  fineqvnttrclse  35460  tz9.1regs  35470  subfacf  35566  subfacp1lem6  35576  cvmsss2  35665  cvmliftlem1  35676  nmulr0  36586  ixpeq12i  36602  ttciunun  36911  bj-rabtr  37454  bj-axseprep  37599  relowlssretop  37897  fin2so  38146  matunitlindflem1  38155  ptrest  38158  poimirlem23  38182  poimirlem24  38183  poimirlem27  38186  poimirlem30  38189  poimirlem32  38191  cnambfre  38207  upixp  38268  0totbnd  38312  prdsbnd  38332  prdstotbnd  38333  cntotbnd  38335  rrnequiv  38374  ac6s6  38711  dmsucmap  39007  disjimeceqim  39343  cdlemefrs32fva  41064  cdlemkid5  41599  cdlemk56  41635  dihf11lem  41930  addinvcom  43083  0dioph  43401  vdioph  43402  pw2f1ocnv  43656  pwinfi  44182  eliunov2  44297  fvmptiunrelexplb0d  44302  fvmptiunrelexplb1d  44304  iunrelexp0  44320  ntrrn  44740  dssmapntrcls  44746  mnurndlem1  44883  rankrelp  45561  0elaxnul  45584  prclaxpr  45586  uniclaxun  45587  omssaxinf2  45589  wessf1ornlem  45795  axccdom  45830  fnmptif  45872  fsumiunss  46183  limcdm0  46226  liminfval2  46374  liminflelimsuplem  46381  cnrefiisplem  46435  0cnf  46483  dvsinax  46519  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  dvnprodlem3  46554  iblempty  46571  fourierdlem89  46801  fourierdlem91  46803  fourierdlem100  46812  fourierdlem108  46820  fourierdlem112  46824  salexct3  46948  salgensscntex  46950  omeiunle  47123  0ome  47135  hoissrrn  47155  ovn0  47172  hoissrrn2  47184  hspmbl  47235  ovolval5lem2  47259  iunhoiioolem  47281  vonioolem2  47287  vonicclem2  47290  smflimlem1  47377  smfsuplem1  47417  smfinflem  47423  smflimsuplem1  47426  smflimsuplem2  47427  smflimsuplem3  47428  smflimsuplem4  47429  smflimsuplem5  47430  smflimsuplem7  47432  smfliminflem  47436  nthrucw  47494  ralndv2  47732  iccelpart  48071  eliunxp2  48999  1arymaptf1  49307  iinxp  49494  iinfssclem2  49718  iinfssclem3  49719  iinfssc  49720  imasubclem1  49767