Theorem rgenw 3071

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

Syntax hints:   ∈ wcel 2108  ∀wral 3067

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

This theorem depends on definitions:  df-bi 207  df-ral 3068

This theorem is referenced by:  rgen2w  3072  reuss  4346  reuun1  4347  rabnc  4414  riinrab  5107  0disj  5159  iinexg  5366  epse  5682  xpiindi  5860  eliunxp  5862  opeliunxp2  5863  elrnmpti  5985  cnviin  6317  fnmpti  6723  eqfnfv  7064  eufnfv  7266  mpoeq12  7523  porpss  7762  iunex  8009  abrexex2  8010  mpoex  8120  suppssov1  8238  suppssov2  8239  suppssfv  8243  opeliunxp2f  8251  onnseq  8400  ixpssmap  8990  boxcutc  8999  nneneq  9272  nneneqOLD  9284  finsschain  9429  dfom3  9716  cantnfdm  9733  rankuni2b  9922  rankval4  9936  alephf1  10154  dfac4  10191  dfacacn  10211  infmap2  10286  cfeq0  10325  fin23lem28  10409  axdc2lem  10517  axcclem  10526  ac6  10549  iundom  10611  konigthlem  10637  iunctb  10643  tskmid  10909  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  uzf  12906  seqof  14110  hashbclem  14501  rlimclim1  15591  fsumcom2  15822  ackbijnn  15876  fprodcom2  16032  lcmf0  16681  phisum  16837  sumhash  16943  ramcl  17076  prdsvallem  17514  prdsval  17515  prdsbas  17517  prdshom  17527  imasplusg  17577  imasmulr  17578  imasvsca  17580  imasip  17581  imasaddfnlem  17588  imasvscafn  17597  isfunc  17928  wunfunc  17965  wunfuncOLD  17966  isnat  18015  natffn  18017  wunnat  18024  wunnatOLD  18025  fucsect  18042  setcepi  18155  grpinvfval  19018  odfval  19574  dfod2  19606  ghmcyg  19938  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  dmdprd  20042  dprdval  20047  dprdf11  20067  dprd2d2  20088  dpjeq  20103  pgpfac1lem2  20119  pgpfac1lem3  20121  pgpfac1lem4  20122  mptscmfsupp0  20947  00lsp  21002  ocv0  21718  ofco2  22478  tgidm  23008  pptbas  23036  tgrest  23188  iscnp2  23268  ist1-3  23378  discmp  23427  1stcfb  23474  lly1stc  23525  disllycmp  23527  dis1stc  23528  comppfsc  23561  txbas  23596  ptbasfi  23610  ptpjopn  23641  dfac14  23647  ptrescn  23668  xkoptsub  23683  fclsval  24037  ptcmplem2  24082  ptcmplem3  24083  cnextrel  24092  tsmsfbas  24157  ustuqtop  24276  prdsxmetlem  24399  ressprdsds  24402  prdsxmslem2  24563  zcld  24854  xrge0tsms  24875  metdsf  24889  metdsge  24890  minveclem1  25477  minveclem3b  25481  minveclem6  25487  uniioombllem4  25640  uniioombllem6  25642  ismbf3d  25708  i1f1lem  25743  reldv  25925  ellimc2  25932  limcflf  25936  limciun  25949  dvfval  25952  dvrec  26013  dvlipcn  26053  mdegle0  26136  ply1nzb  26182  quotlem  26360  taylfval  26418  ulmdvlem1  26461  ulmdvlem2  26462  ulmdvlem3  26463  psercn  26488  sqff1o  27243  lgsquadlem2  27443  disjxwwlksn  29937  disjxwwlkn  29946  numclwwlk3lem2  30416  grpoidval  30545  grpoidinv2  30547  grpoinv  30557  minvecolem1  30906  minvecolem5  30913  minvecolem6  30914  adjbdln  32115  dfcnv2  32694  intimafv  32722  rexdiv  32890  gsumpart  33038  xrge0tsmsd  33041  fedgmullem2  33643  irngval  33685  rspectopn  33813  zarcls  33820  zartopn  33821  esumnul  34012  esum0  34013  hasheuni  34049  esum2d  34057  ldgenpisyslem3  34129  measvuni  34178  measdivcstALTV  34189  ddemeas  34200  carsgclctunlem2  34284  eulerpartlemgs2  34345  probfinmeasbALTV  34394  0rrv  34416  signsplypnf  34527  signsply0  34528  hgt750lemb  34633  bnj226  34710  bnj98  34843  bnj517  34861  bnj893  34904  bnj1137  34971  subfacf  35143  subfacp1lem6  35153  cvmsss2  35242  cvmliftlem1  35253  ixpeq12i  36165  bj-rabtr  36896  relowlssretop  37329  fin2so  37567  matunitlindflem1  37576  ptrest  37579  poimirlem23  37603  poimirlem24  37604  poimirlem27  37607  poimirlem30  37610  poimirlem32  37612  cnambfre  37628  upixp  37689  0totbnd  37733  prdsbnd  37753  prdstotbnd  37754  cntotbnd  37756  rrnequiv  37795  ac6s6  38132  cdlemefrs32fva  40357  cdlemkid5  40892  cdlemk56  40928  dihf11lem  41223  addinvcom  42407  0dioph  42734  vdioph  42735  rmxyelqirrOLD  42867  pw2f1ocnv  42994  pwinfi  43526  eliunov2  43641  fvmptiunrelexplb0d  43646  fvmptiunrelexplb1d  43648  iunrelexp0  43664  ntrrn  44084  dssmapntrcls  44090  mnurndlem1  44250  wessf1ornlem  45092  axccdom  45129  mpteq1dfOLD  45144  fnmptif  45175  fsumiunss  45496  limcdm0  45539  liminfval2  45689  liminflelimsuplem  45696  cnrefiisplem  45750  0cnf  45798  dvsinax  45834  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem3  45869  iblempty  45886  fourierdlem89  46116  fourierdlem91  46118  fourierdlem100  46127  fourierdlem108  46135  fourierdlem112  46139  salexct3  46263  salgensscntex  46265  omeiunle  46438  0ome  46450  hoissrrn  46470  ovn0  46487  hoissrrn2  46499  hspmbl  46550  ovolval5lem2  46574  iunhoiioolem  46596  vonioolem2  46602  vonicclem2  46605  smflimlem1  46692  smfsuplem1  46732  smfinflem  46738  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem3  46743  smflimsuplem4  46744  smflimsuplem5  46745  smflimsuplem7  46747  smfliminflem  46751  ralndv2  47021  iccelpart  47307  eliunxp2  48058  1arymaptf1  48376