Theorem rgenw 3053

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

Syntax hints:   ∈ wcel 2113  ∀wral 3049

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 207  df-ral 3050

This theorem is referenced by:  rgen2w  3054  reuss  4277  reuun1  4278  rabnc  4341  riinrab  5037  0disj  5089  iinexg  5291  epse  5604  xpiindi  5782  eliunxp  5784  opeliunxp2  5785  elrnmpti  5909  cnviin  6242  fnmpti  6633  eqfnfv  6974  eufnfv  7173  mpoeq12  7429  porpss  7670  iunex  7910  abrexex2  7911  mpoex  8021  suppssov1  8137  suppssov2  8138  suppssfv  8142  opeliunxp2f  8150  onnseq  8274  ixpssmap  8868  boxcutc  8877  nneneq  9128  finsschain  9257  dfom3  9554  cantnfdm  9571  rankuni2b  9763  rankval4  9777  alephf1  9993  dfac4  10030  dfacacn  10050  infmap2  10125  cfeq0  10164  fin23lem28  10248  axdc2lem  10356  axcclem  10365  ac6  10388  iundom  10450  konigthlem  10477  iunctb  10483  tskmid  10749  supaddc  12107  supadd  12108  supmul1  12109  supmullem2  12111  supmul  12112  uzf  12752  seqof  13980  hashbclem  14373  rlimclim1  15466  fsumcom2  15695  ackbijnn  15749  fprodcom2  15905  lcmf0  16559  phisum  16716  sumhash  16822  ramcl  16955  prdsvallem  17372  prdsval  17373  prdsbas  17375  prdshom  17385  imasplusg  17436  imasmulr  17437  imasvsca  17439  imasip  17440  imasaddfnlem  17447  imasvscafn  17456  isfunc  17786  wunfunc  17823  isnat  17872  natffn  17874  wunnat  17881  fucsect  17897  setcepi  18010  grpinvfval  18906  odfval  19459  dfod2  19491  ghmcyg  19823  gsum2d2lem  19900  gsum2d2  19901  gsumcom2  19902  dmdprd  19927  dprdval  19932  dprdf11  19952  dprd2d2  19973  dpjeq  19988  pgpfac1lem2  20004  pgpfac1lem3  20006  pgpfac1lem4  20007  mptscmfsupp0  20876  00lsp  20930  ocv0  21630  ofco2  22393  tgidm  22922  pptbas  22950  tgrest  23101  iscnp2  23181  ist1-3  23291  discmp  23340  1stcfb  23387  lly1stc  23438  disllycmp  23440  dis1stc  23441  comppfsc  23474  txbas  23509  ptbasfi  23523  ptpjopn  23554  dfac14  23560  ptrescn  23581  xkoptsub  23596  fclsval  23950  ptcmplem2  23995  ptcmplem3  23996  cnextrel  24005  tsmsfbas  24070  ustuqtop  24188  prdsxmetlem  24310  ressprdsds  24313  prdsxmslem2  24471  zcld  24756  xrge0tsms  24777  metdsf  24791  metdsge  24792  minveclem1  25378  minveclem3b  25382  minveclem6  25388  uniioombllem4  25541  uniioombllem6  25543  ismbf3d  25609  i1f1lem  25644  reldv  25825  ellimc2  25832  limcflf  25836  limciun  25849  dvfval  25852  dvrec  25913  dvlipcn  25953  mdegle0  26036  ply1nzb  26082  quotlem  26262  taylfval  26320  ulmdvlem1  26363  ulmdvlem2  26364  ulmdvlem3  26365  psercn  26390  sqff1o  27146  lgsquadlem2  27346  bdayiun  27887  disjxwwlksn  29926  disjxwwlkn  29935  numclwwlk3lem2  30408  grpoidval  30537  grpoidinv2  30539  grpoinv  30549  minvecolem1  30898  minvecolem5  30905  minvecolem6  30906  adjbdln  32107  dfcnv2  32703  intimafv  32739  rexdiv  32956  gsumpart  33095  xrge0tsmsd  33104  fedgmullem2  33736  irngval  33791  rspectopn  33973  zarcls  33980  zartopn  33981  esumnul  34154  esum0  34155  hasheuni  34191  esum2d  34199  ldgenpisyslem3  34271  measvuni  34320  measdivcstALTV  34331  ddemeas  34342  carsgclctunlem2  34425  eulerpartlemgs2  34486  probfinmeasbALTV  34535  0rrv  34557  signsplypnf  34656  signsply0  34657  hgt750lemb  34762  bnj226  34839  bnj98  34972  bnj517  34990  bnj893  35033  bnj1137  35100  rankval4b  35205  rankfilimbi  35206  fineqvnttrclse  35229  tz9.1regs  35239  subfacf  35318  subfacp1lem6  35328  cvmsss2  35417  cvmliftlem1  35428  ixpeq12i  36344  bj-rabtr  37074  relowlssretop  37507  fin2so  37747  matunitlindflem1  37756  ptrest  37759  poimirlem23  37783  poimirlem24  37784  poimirlem27  37787  poimirlem30  37790  poimirlem32  37792  cnambfre  37808  upixp  37869  0totbnd  37913  prdsbnd  37933  prdstotbnd  37934  cntotbnd  37936  rrnequiv  37975  ac6s6  38312  dmsucmap  38581  cdlemefrs32fva  40599  cdlemkid5  41134  cdlemk56  41170  dihf11lem  41465  addinvcom  42629  0dioph  42962  vdioph  42963  pw2f1ocnv  43221  pwinfi  43747  eliunov2  43862  fvmptiunrelexplb0d  43867  fvmptiunrelexplb1d  43869  iunrelexp0  43885  ntrrn  44305  dssmapntrcls  44311  mnurndlem1  44464  rankrelp  45143  0elaxnul  45166  prclaxpr  45168  uniclaxun  45169  omssaxinf2  45171  wessf1ornlem  45371  axccdom  45408  fnmptif  45451  fsumiunss  45763  limcdm0  45806  liminfval2  45954  liminflelimsuplem  45961  cnrefiisplem  46015  0cnf  46063  dvsinax  46099  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnprodlem3  46134  iblempty  46151  fourierdlem89  46381  fourierdlem91  46383  fourierdlem100  46392  fourierdlem108  46400  fourierdlem112  46404  salexct3  46528  salgensscntex  46530  omeiunle  46703  0ome  46715  hoissrrn  46735  ovn0  46752  hoissrrn2  46764  hspmbl  46815  ovolval5lem2  46839  iunhoiioolem  46861  vonioolem2  46867  vonicclem2  46870  smflimlem1  46957  smfsuplem1  46997  smfinflem  47003  smflimsuplem1  47006  smflimsuplem2  47007  smflimsuplem3  47008  smflimsuplem4  47009  smflimsuplem5  47010  smflimsuplem7  47012  smfliminflem  47016  nthrucw  47072  ralndv2  47294  iccelpart  47621  eliunxp2  48522  1arymaptf1  48830  iinxp  49018  iinfssclem2  49242  iinfssclem3  49243  iinfssc  49244  imasubclem1  49291