Theorem rgenw 3077

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

Syntax hints:   ∈ wcel 2107  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-ral 3070

This theorem is referenced by:  rgen2w  3078  reuss  4251  reuun1  4252  rabnc  4322  riinrab  5014  0disj  5067  iinexg  5266  epse  5573  xpiindi  5747  eliunxp  5749  opeliunxp2  5750  elrnmpti  5872  cnviin  6193  fnmpti  6585  eqfnfv  6918  mptexgf  7107  eufnfv  7114  mpoeq12  7357  porpss  7589  iunex  7820  abrexex2  7821  mpoex  7929  suppssov1  8023  suppssfv  8027  opeliunxp2f  8035  onnseq  8184  ixpssmap  8729  boxcutc  8738  nneneq  9001  nneneqOLD  9013  finsschain  9135  dfom3  9414  cantnfdm  9431  rankuni2b  9620  rankval4  9634  alephf1  9850  dfac4  9887  dfacacn  9906  infmap2  9983  cfeq0  10021  fin23lem28  10105  axdc2lem  10213  axcclem  10222  ac6  10245  iundom  10307  konigthlem  10333  iunctb  10339  tskmid  10605  supaddc  11951  supadd  11952  supmul1  11953  supmullem2  11955  supmul  11956  uzf  12594  seqof  13789  hashbclem  14173  rlimclim1  15263  fsumcom2  15495  ackbijnn  15549  fprodcom2  15703  lcmf0  16348  phisum  16500  sumhash  16606  ramcl  16739  prdsvallem  17174  prdsval  17175  prdsbas  17177  prdshom  17187  imasplusg  17237  imasmulr  17238  imasvsca  17240  imasip  17241  imasaddfnlem  17248  imasvscafn  17257  isfunc  17588  wunfunc  17623  wunfuncOLD  17624  isnat  17672  natffn  17674  wunnat  17681  wunnatOLD  17682  fucsect  17699  setcepi  17812  grpinvfval  18627  odfval  19149  dfod2  19180  ghmcyg  19506  gsum2d2lem  19583  gsum2d2  19584  gsumcom2  19585  dmdprd  19610  dprdval  19615  dprdf11  19635  dprd2d2  19656  dpjeq  19671  pgpfac1lem2  19687  pgpfac1lem3  19689  pgpfac1lem4  19690  mptscmfsupp0  20197  00lsp  20252  ocv0  20891  ofco2  21609  tgidm  22139  pptbas  22167  tgrest  22319  iscnp2  22399  ist1-3  22509  discmp  22558  1stcfb  22605  lly1stc  22656  disllycmp  22658  dis1stc  22659  comppfsc  22692  txbas  22727  ptbasfi  22741  ptpjopn  22772  dfac14  22778  ptrescn  22799  xkoptsub  22814  fclsval  23168  ptcmplem2  23213  ptcmplem3  23214  cnextrel  23223  tsmsfbas  23288  ustuqtop  23407  prdsxmetlem  23530  ressprdsds  23533  prdsxmslem2  23694  zcld  23985  xrge0tsms  24006  metdsf  24020  metdsge  24021  minveclem1  24597  minveclem3b  24601  minveclem6  24607  uniioombllem4  24759  uniioombllem6  24761  ismbf3d  24827  i1f1lem  24862  reldv  25043  ellimc2  25050  limcflf  25054  limciun  25067  dvfval  25070  dvrec  25128  dvlipcn  25167  mdegle0  25251  ply1nzb  25296  quotlem  25469  taylfval  25527  ulmdvlem1  25568  ulmdvlem2  25569  ulmdvlem3  25570  psercn  25594  sqff1o  26340  lgsquadlem2  26538  disjxwwlksn  28278  wwlksnfi  28280  disjxwwlkn  28287  numclwwlk3lem2  28757  grpoidval  28884  grpoidinv2  28886  grpoinv  28896  minvecolem1  29245  minvecolem5  29252  minvecolem6  29253  adjbdln  30454  dfcnv2  31022  intimafv  31052  rexdiv  31209  gsumpart  31324  xrge0tsmsd  31326  fedgmullem2  31720  rspectopn  31826  zarcls  31833  zartopn  31834  esumnul  32025  esum0  32026  hasheuni  32062  esum2d  32070  ldgenpisyslem3  32142  measvuni  32191  measdivcstALTV  32202  ddemeas  32213  carsgclctunlem2  32295  eulerpartlemgs2  32356  probfinmeasbALTV  32405  0rrv  32427  signsplypnf  32538  signsply0  32539  hgt750lemb  32645  bnj226  32722  bnj98  32856  bnj517  32874  bnj893  32917  bnj1137  32984  subfacf  33146  subfacp1lem6  33156  cvmsss2  33245  cvmliftlem1  33256  bj-rabtr  35127  relowlssretop  35543  fin2so  35773  matunitlindflem1  35782  ptrest  35785  poimirlem23  35809  poimirlem24  35810  poimirlem27  35813  poimirlem30  35816  poimirlem32  35818  cnambfre  35834  upixp  35896  0totbnd  35940  prdsbnd  35960  prdstotbnd  35961  cntotbnd  35963  rrnequiv  36002  ac6s6  36339  cdlemefrs32fva  38421  cdlemkid5  38956  cdlemk56  38992  dihf11lem  39287  addinvcom  40420  0dioph  40607  vdioph  40608  rmxyelqirr  40739  pw2f1ocnv  40866  pwinfi  41178  eliunov2  41294  fvmptiunrelexplb0d  41299  fvmptiunrelexplb1d  41301  iunrelexp0  41317  ntrrn  41739  dssmapntrcls  41745  mnurndlem1  41906  wessf1ornlem  42729  axccdom  42769  mpteq1dfOLD  42787  fsumiunss  43123  limcdm0  43166  liminfval2  43316  liminflelimsuplem  43323  cnrefiisplem  43377  0cnf  43425  dvsinax  43461  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem3  43496  iblempty  43513  fourierdlem89  43743  fourierdlem91  43745  fourierdlem100  43754  fourierdlem108  43762  fourierdlem112  43766  salexct3  43888  salgensscntex  43890  omeiunle  44062  0ome  44074  hoissrrn  44094  ovn0  44111  hoissrrn2  44123  hspmbl  44174  ovolval5lem2  44198  ovolval5lem3  44199  iunhoiioolem  44220  vonioolem2  44226  vonicclem2  44229  smflimlem1  44316  smfsuplem1  44355  smfinflem  44361  smflimsuplem1  44364  smflimsuplem2  44365  smflimsuplem3  44366  smflimsuplem4  44367  smflimsuplem5  44368  smflimsuplem7  44370  smfliminflem  44374  ralndv2  44609  iccelpart  44896  eliunxp2  45680  1arymaptf1  45999