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  35438  fineqvnttrclse  35470  tz9.1regs  35480  subfacf  35600  subfacp1lem6  35610  cvmsss2  35699  cvmliftlem1  35710  nmulr0  36620  ixpeq12i  36636  ttciunun  36945  bj-rabtr  37488  bj-axseprep  37633  relowlssretop  37931  fin2so  38180  matunitlindflem1  38189  ptrest  38192  poimirlem23  38216  poimirlem24  38217  poimirlem27  38220  poimirlem30  38223  poimirlem32  38225  cnambfre  38241  upixp  38302  0totbnd  38346  prdsbnd  38366  prdstotbnd  38367  cntotbnd  38369  rrnequiv  38408  ac6s6  38745  dmsucmap  39041  disjimeceqim  39377  cdlemefrs32fva  41098  cdlemkid5  41633  cdlemk56  41669  dihf11lem  41964  addinvcom  43117  0dioph  43435  vdioph  43436  pw2f1ocnv  43690  pwinfi  44216  eliunov2  44331  fvmptiunrelexplb0d  44336  fvmptiunrelexplb1d  44338  iunrelexp0  44354  ntrrn  44774  dssmapntrcls  44780  mnurndlem1  44917  rankrelp  45595  0elaxnul  45618  prclaxpr  45620  uniclaxun  45621  omssaxinf2  45623  wessf1ornlem  45829  axccdom  45864  fnmptif  45906  fsumiunss  46217  limcdm0  46260  liminfval2  46408  liminflelimsuplem  46415  cnrefiisplem  46469  0cnf  46517  dvsinax  46553  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  dvnprodlem3  46588  iblempty  46605  fourierdlem89  46835  fourierdlem91  46837  fourierdlem100  46846  fourierdlem108  46854  fourierdlem112  46858  salexct3  46982  salgensscntex  46984  omeiunle  47157  0ome  47169  hoissrrn  47189  ovn0  47206  hoissrrn2  47218  hspmbl  47269  ovolval5lem2  47293  iunhoiioolem  47315  vonioolem2  47321  vonicclem2  47324  smflimlem1  47411  smfsuplem1  47451  smfinflem  47457  smflimsuplem1  47460  smflimsuplem2  47461  smflimsuplem3  47462  smflimsuplem4  47463  smflimsuplem5  47464  smflimsuplem7  47466  smfliminflem  47470  nthrucw  47528  ralndv2  47766  iccelpart  48105  eliunxp2  49033  1arymaptf1  49341  iinxp  49528  iinfssclem2  49752  iinfssclem3  49753  iinfssc  49754  imasubclem1  49801