Theorem rgenw 3048

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044

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 3045

This theorem is referenced by:  rgen2w  3049  reuss  4286  reuun1  4287  rabnc  4350  riinrab  5043  0disj  5095  iinexg  5298  epse  5613  xpiindi  5789  eliunxp  5791  opeliunxp2  5792  elrnmpti  5915  cnviin  6247  fnmpti  6643  eqfnfv  6985  eufnfv  7185  mpoeq12  7442  porpss  7683  iunex  7926  abrexex2  7927  mpoex  8037  suppssov1  8153  suppssov2  8154  suppssfv  8158  opeliunxp2f  8166  onnseq  8290  ixpssmap  8882  boxcutc  8891  nneneq  9147  finsschain  9286  dfom3  9576  cantnfdm  9593  rankuni2b  9782  rankval4  9796  alephf1  10014  dfac4  10051  dfacacn  10071  infmap2  10146  cfeq0  10185  fin23lem28  10269  axdc2lem  10377  axcclem  10386  ac6  10409  iundom  10471  konigthlem  10497  iunctb  10503  tskmid  10769  supaddc  12126  supadd  12127  supmul1  12128  supmullem2  12130  supmul  12131  uzf  12772  seqof  14000  hashbclem  14393  rlimclim1  15487  fsumcom2  15716  ackbijnn  15770  fprodcom2  15926  lcmf0  16580  phisum  16737  sumhash  16843  ramcl  16976  prdsvallem  17393  prdsval  17394  prdsbas  17396  prdshom  17406  imasplusg  17456  imasmulr  17457  imasvsca  17459  imasip  17460  imasaddfnlem  17467  imasvscafn  17476  isfunc  17806  wunfunc  17843  isnat  17892  natffn  17894  wunnat  17901  fucsect  17917  setcepi  18030  grpinvfval  18892  odfval  19446  dfod2  19478  ghmcyg  19810  gsum2d2lem  19887  gsum2d2  19888  gsumcom2  19889  dmdprd  19914  dprdval  19919  dprdf11  19939  dprd2d2  19960  dpjeq  19975  pgpfac1lem2  19991  pgpfac1lem3  19993  pgpfac1lem4  19994  mptscmfsupp0  20865  00lsp  20919  ocv0  21619  ofco2  22371  tgidm  22900  pptbas  22928  tgrest  23079  iscnp2  23159  ist1-3  23269  discmp  23318  1stcfb  23365  lly1stc  23416  disllycmp  23418  dis1stc  23419  comppfsc  23452  txbas  23487  ptbasfi  23501  ptpjopn  23532  dfac14  23538  ptrescn  23559  xkoptsub  23574  fclsval  23928  ptcmplem2  23973  ptcmplem3  23974  cnextrel  23983  tsmsfbas  24048  ustuqtop  24167  prdsxmetlem  24289  ressprdsds  24292  prdsxmslem2  24450  zcld  24735  xrge0tsms  24756  metdsf  24770  metdsge  24771  minveclem1  25357  minveclem3b  25361  minveclem6  25367  uniioombllem4  25520  uniioombllem6  25522  ismbf3d  25588  i1f1lem  25623  reldv  25804  ellimc2  25811  limcflf  25815  limciun  25828  dvfval  25831  dvrec  25892  dvlipcn  25932  mdegle0  26015  ply1nzb  26061  quotlem  26241  taylfval  26299  ulmdvlem1  26342  ulmdvlem2  26343  ulmdvlem3  26344  psercn  26369  sqff1o  27125  lgsquadlem2  27325  bdayiun  27864  disjxwwlksn  29884  disjxwwlkn  29893  numclwwlk3lem2  30363  grpoidval  30492  grpoidinv2  30494  grpoinv  30504  minvecolem1  30853  minvecolem5  30860  minvecolem6  30861  adjbdln  32062  dfcnv2  32650  intimafv  32684  rexdiv  32896  gsumpart  33040  xrge0tsmsd  33045  fedgmullem2  33619  irngval  33673  rspectopn  33850  zarcls  33857  zartopn  33858  esumnul  34031  esum0  34032  hasheuni  34068  esum2d  34076  ldgenpisyslem3  34148  measvuni  34197  measdivcstALTV  34208  ddemeas  34219  carsgclctunlem2  34303  eulerpartlemgs2  34364  probfinmeasbALTV  34413  0rrv  34435  signsplypnf  34534  signsply0  34535  hgt750lemb  34640  bnj226  34717  bnj98  34850  bnj517  34868  bnj893  34911  bnj1137  34978  subfacf  35155  subfacp1lem6  35165  cvmsss2  35254  cvmliftlem1  35265  ixpeq12i  36182  bj-rabtr  36911  relowlssretop  37344  fin2so  37594  matunitlindflem1  37603  ptrest  37606  poimirlem23  37630  poimirlem24  37631  poimirlem27  37634  poimirlem30  37637  poimirlem32  37639  cnambfre  37655  upixp  37716  0totbnd  37760  prdsbnd  37780  prdstotbnd  37781  cntotbnd  37783  rrnequiv  37822  ac6s6  38159  cdlemefrs32fva  40387  cdlemkid5  40922  cdlemk56  40958  dihf11lem  41253  addinvcom  42413  0dioph  42759  vdioph  42760  rmxyelqirrOLD  42892  pw2f1ocnv  43019  pwinfi  43546  eliunov2  43661  fvmptiunrelexplb0d  43666  fvmptiunrelexplb1d  43668  iunrelexp0  43684  ntrrn  44104  dssmapntrcls  44110  mnurndlem1  44263  rankrelp  44943  0elaxnul  44966  prclaxpr  44968  uniclaxun  44969  omssaxinf2  44971  wessf1ornlem  45172  axccdom  45209  fnmptif  45252  fsumiunss  45566  limcdm0  45609  liminfval2  45759  liminflelimsuplem  45766  cnrefiisplem  45820  0cnf  45868  dvsinax  45904  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnprodlem3  45939  iblempty  45956  fourierdlem89  46186  fourierdlem91  46188  fourierdlem100  46197  fourierdlem108  46205  fourierdlem112  46209  salexct3  46333  salgensscntex  46335  omeiunle  46508  0ome  46520  hoissrrn  46540  ovn0  46557  hoissrrn2  46569  hspmbl  46620  ovolval5lem2  46644  iunhoiioolem  46666  vonioolem2  46672  vonicclem2  46675  smflimlem1  46762  smfsuplem1  46802  smfinflem  46808  smflimsuplem1  46811  smflimsuplem2  46812  smflimsuplem3  46813  smflimsuplem4  46814  smflimsuplem5  46815  smflimsuplem7  46817  smfliminflem  46821  ralndv2  47100  iccelpart  47427  eliunxp2  48315  1arymaptf1  48624  iinxp  48812  iinfssclem2  49037  iinfssclem3  49038  iinfssc  49039  imasubclem1  49086