Theorem rgenw 3150

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

Syntax hints:   ∈ wcel 2114  ∀wral 3138

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

This theorem depends on definitions:  df-bi 209  df-ral 3143

This theorem is referenced by:  rgen2w  3151  reuss  4284  reuun1  4285  rabnc  4341  riinrab  5006  0disj  5058  iinexg  5244  epse  5538  xpiindi  5706  eliunxp  5708  opeliunxp2  5709  elrnmpti  5832  cnviin  6137  fnmpti  6491  eqfnfv  6802  mptexgf  6985  eufnfv  6991  mpoeq12  7227  porpss  7453  iunex  7669  abrexex2  7670  mpoex  7777  suppssov1  7862  suppssfv  7866  opeliunxp2f  7876  onnseq  7981  ixpssmap  8496  boxcutc  8505  nneneq  8700  finsschain  8831  dfom3  9110  cantnfdm  9127  rankuni2b  9282  rankval4  9296  alephf1  9511  dfac4  9548  dfacacn  9567  infmap2  9640  cfeq0  9678  fin23lem28  9762  axdc2lem  9870  axcclem  9879  ac6  9902  iundom  9964  konigthlem  9990  iunctb  9996  tskmid  10262  supaddc  11608  supadd  11609  supmul1  11610  supmullem2  11612  supmul  11613  uzf  12247  seqof  13428  hashbclem  13811  wrdexgOLD  13873  rlimclim1  14902  fsumcom2  15129  ackbijnn  15183  fprodcom2  15338  lcmf0  15978  phisum  16127  sumhash  16232  ramcl  16365  prdsval  16728  prdsbas  16730  prdshom  16740  imasplusg  16790  imasmulr  16791  imasvsca  16793  imasip  16794  imasaddfnlem  16801  imasvscafn  16810  isfunc  17134  wunfunc  17169  isnat  17217  natffn  17219  wunnat  17226  fucsect  17242  setcepi  17348  grpinvfval  18142  odfval  18660  dfod2  18691  ghmcyg  19016  gsum2d2lem  19093  gsum2d2  19094  gsumcom2  19095  dmdprd  19120  dprdval  19125  dprdf11  19145  dprd2d2  19166  dpjeq  19181  pgpfac1lem2  19197  pgpfac1lem3  19199  pgpfac1lem4  19200  mptscmfsupp0  19699  00lsp  19753  ocv0  20821  ofco2  21060  tgidm  21588  pptbas  21616  tgrest  21767  iscnp2  21847  ist1-3  21957  discmp  22006  1stcfb  22053  lly1stc  22104  disllycmp  22106  dis1stc  22107  comppfsc  22140  txbas  22175  ptbasfi  22189  ptpjopn  22220  dfac14  22226  ptrescn  22247  xkoptsub  22262  fclsval  22616  ptcmplem2  22661  ptcmplem3  22662  cnextrel  22671  tsmsfbas  22736  ustuqtop  22855  prdsxmetlem  22978  ressprdsds  22981  prdsxmslem2  23139  zcld  23421  xrge0tsms  23442  metdsf  23456  metdsge  23457  minveclem1  24027  minveclem3b  24031  minveclem6  24037  uniioombllem4  24187  uniioombllem6  24189  ismbf3d  24255  i1f1lem  24290  reldv  24468  ellimc2  24475  limcflf  24479  limciun  24492  dvfval  24495  dvrec  24552  dvlipcn  24591  mdegle0  24671  ply1nzb  24716  quotlem  24889  taylfval  24947  ulmdvlem1  24988  ulmdvlem2  24989  ulmdvlem3  24990  psercn  25014  sqff1o  25759  lgsquadlem2  25957  disjxwwlksn  27682  wwlksnfi  27684  wwlksnfiOLD  27685  disjxwwlkn  27692  numclwwlk3lem2  28163  grpoidval  28290  grpoidinv2  28292  grpoinv  28302  minvecolem1  28651  minvecolem5  28658  minvecolem6  28659  adjbdln  29860  dfcnv2  30422  rexdiv  30602  xrge0tsmsd  30692  fedgmullem2  31026  esumnul  31307  esum0  31308  hasheuni  31344  esum2d  31352  ldgenpisyslem3  31424  measvuni  31473  measdivcstALTV  31484  ddemeas  31495  carsgclctunlem2  31577  eulerpartlemgs2  31638  probfinmeasbALTV  31687  0rrv  31709  signsplypnf  31820  signsply0  31821  hgt750lemb  31927  bnj226  32004  bnj98  32139  bnj517  32157  bnj893  32200  bnj1137  32267  subfacf  32422  subfacp1lem6  32432  cvmsss2  32521  cvmliftlem1  32532  nulssgt  33263  bj-rabtr  34251  relowlssretop  34647  fin2so  34894  matunitlindflem1  34903  ptrest  34906  poimirlem23  34930  poimirlem24  34931  poimirlem27  34934  poimirlem30  34937  poimirlem32  34939  cnambfre  34955  upixp  35019  0totbnd  35066  prdsbnd  35086  prdstotbnd  35087  cntotbnd  35089  rrnequiv  35128  ac6s6  35465  cdlemefrs32fva  37551  cdlemkid5  38086  cdlemk56  38122  dihf11lem  38417  0dioph  39424  vdioph  39425  rmxyelqirr  39556  pw2f1ocnv  39683  pwinfi  39972  eliunov2  40073  fvmptiunrelexplb0d  40078  fvmptiunrelexplb1d  40080  iunrelexp0  40096  ntrrn  40521  dssmapntrcls  40527  mnurndlem1  40666  wessf1ornlem  41494  axccdom  41536  mpteq1df  41555  fsumiunss  41905  limcdm0  41948  liminfval2  42098  liminflelimsuplem  42105  cnrefiisplem  42159  0cnf  42209  dvsinax  42246  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnprodlem3  42282  iblempty  42299  fourierdlem89  42529  fourierdlem91  42531  fourierdlem100  42540  fourierdlem108  42548  fourierdlem112  42552  salexct3  42674  salgensscntex  42676  omeiunle  42848  0ome  42860  hoissrrn  42880  ovn0  42897  hoissrrn2  42909  hspmbl  42960  ovolval5lem2  42984  ovolval5lem3  42985  iunhoiioolem  43006  vonioolem2  43012  vonicclem2  43015  smflimlem1  43096  smfsuplem1  43134  smfinflem  43140  smflimsuplem1  43143  smflimsuplem2  43144  smflimsuplem3  43145  smflimsuplem4  43146  smflimsuplem5  43147  smflimsuplem7  43149  smfliminflem  43153  ralndv2  43354  iccelpart  43642  eliunxp2  44431