Theorem rgenw 3094

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

Syntax hints:   ∈ wcel 2048  ∀wral 3082

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

This theorem depends on definitions:  df-bi 199  df-ral 3087

This theorem is referenced by:  rgen2w  3095  reuss  4166  reuun1  4167  rabnc  4222  riinrab  4866  0disj  4916  iinexg  5094  epse  5383  xpiindi  5549  eliunxp  5551  opeliunxp2  5552  elrnmpti  5668  cnviin  5969  fnmpti  6315  eqfnfv  6621  mptexgf  6805  eufnfv  6811  mpoeq12  7039  porpss  7265  iunex  7474  abrexex2  7475  mpoex  7578  suppssov1  7658  suppssfv  7662  opeliunxp2f  7672  onnseq  7778  ixpssmap  8285  boxcutc  8294  nneneq  8488  finsschain  8618  dfom3  8896  cantnfdm  8913  rankuni2b  9068  rankval4  9082  alephf1  9297  dfac4  9334  dfacacn  9353  infmap2  9430  cfeq0  9468  fin23lem28  9552  axdc2lem  9660  axcclem  9669  ac6  9692  iundom  9754  konigthlem  9780  iunctb  9786  tskmid  10052  supaddc  11401  supadd  11402  supmul1  11403  supmullem2  11405  supmul  11406  uzf  12054  seqof  13235  hashbclem  13613  wrdexgOLD  13673  rlimclim1  14753  fsumcom2  14979  ackbijnn  15033  fprodcom2  15188  lcmf0  15824  phisum  15973  sumhash  16078  ramcl  16211  prdsval  16574  prdsbas  16576  prdshom  16586  imasplusg  16636  imasmulr  16637  imasvsca  16639  imasip  16640  imasaddfnlem  16647  imasvscafn  16656  isfunc  16982  wunfunc  17017  isnat  17065  natffn  17067  wunnat  17074  fucsect  17090  setcepi  17196  grpinvfval  17919  odfval  18412  dfod2  18442  ghmcyg  18760  gsum2d2lem  18836  gsum2d2  18837  gsumcom2  18838  dmdprd  18860  dprdval  18865  dprdf11  18885  dprd2d2  18906  dpjeq  18921  pgpfac1lem2  18937  pgpfac1lem3  18939  pgpfac1lem4  18940  mptscmfsupp0  19411  00lsp  19465  ocv0  20513  ofco2  20754  tgidm  21282  pptbas  21310  tgrest  21461  iscnp2  21541  ist1-3  21651  discmp  21700  1stcfb  21747  lly1stc  21798  disllycmp  21800  dis1stc  21801  comppfsc  21834  txbas  21869  ptbasfi  21883  ptpjopn  21914  dfac14  21920  ptrescn  21941  xkoptsub  21956  fclsval  22310  ptcmplem2  22355  ptcmplem3  22356  cnextrel  22365  tsmsfbas  22429  ustuqtop  22548  prdsxmetlem  22671  ressprdsds  22674  prdsxmslem2  22832  zcld  23114  xrge0tsms  23135  metdsf  23149  metdsge  23150  minveclem1  23720  minveclem3b  23724  minveclem6  23730  uniioombllem4  23880  uniioombllem6  23882  ismbf3d  23948  i1f1lem  23983  reldv  24161  ellimc2  24168  limcflf  24172  limciun  24185  dvfval  24188  dvrec  24245  dvlipcn  24284  mdegle0  24364  ply1nzb  24409  quotlem  24582  taylfval  24640  ulmdvlem1  24681  ulmdvlem2  24682  ulmdvlem3  24683  psercn  24707  sqff1o  25451  lgsquadlem2  25649  disjxwwlksn  27392  disjxwwlksnOLD  27393  wwlksnfi  27395  wwlksnfiOLD  27396  disjxwwlkn  27407  disjxwwlknOLD  27408  numclwwlk3lem2  27931  grpoidval  28057  grpoidinv2  28059  grpoinv  28069  minvecolem1  28419  minvecolem5  28426  minvecolem6  28427  adjbdln  29631  dfcnv2  30174  rexdiv  30337  xrge0tsmsd  30486  fedgmullem2  30611  esumnul  30908  esum0  30909  hasheuni  30945  esum2d  30953  ldgenpisyslem3  31026  measvuni  31075  measdivcstOLD  31085  ddemeas  31097  carsgclctunlem2  31179  eulerpartlemgs2  31240  probfinmeasbOLD  31289  0rrv  31312  signsplypnf  31427  signsply0  31428  hgt750lemb  31536  bnj226  31613  bnj98  31747  bnj517  31765  bnj893  31808  bnj1137  31873  subfacf  31967  subfacp1lem6  31977  cvmsss2  32066  cvmliftlem1  32077  nulssgt  32724  bj-rabtr  33683  relowlssretop  34021  fin2so  34268  matunitlindflem1  34277  ptrest  34280  poimirlem23  34304  poimirlem24  34305  poimirlem27  34308  poimirlem30  34311  poimirlem32  34313  cnambfre  34329  upixp  34394  0totbnd  34441  prdsbnd  34461  prdstotbnd  34462  cntotbnd  34464  rrnequiv  34503  ac6s6  34842  cdlemefrs32fva  36929  cdlemkid5  37464  cdlemk56  37500  dihf11lem  37795  0dioph  38716  vdioph  38717  rmxyelqirr  38848  pw2f1ocnv  38975  pwinfi  39230  eliunov2  39332  fvmptiunrelexplb0d  39337  fvmptiunrelexplb1d  39339  iunrelexp0  39355  ntrrn  39780  dssmapntrcls  39786  mnurndlem1  39937  wessf1ornlem  40815  axccdom  40858  mpteq1df  40879  fsumiunss  41233  limcdm0  41276  liminfval2  41426  liminflelimsuplem  41433  cnrefiisplem  41487  0cnf  41536  dvsinax  41573  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  dvnprodlem3  41609  iblempty  41626  fourierdlem89  41857  fourierdlem91  41859  fourierdlem100  41868  fourierdlem108  41876  fourierdlem112  41880  salexct3  42002  salgensscntex  42004  omeiunle  42176  0ome  42188  hoissrrn  42208  ovn0  42225  hoissrrn2  42237  hspmbl  42288  ovolval5lem2  42312  ovolval5lem3  42313  iunhoiioolem  42334  vonioolem2  42340  vonicclem2  42343  smflimlem1  42424  smfsuplem1  42462  smfinflem  42468  smflimsuplem1  42471  smflimsuplem2  42472  smflimsuplem3  42473  smflimsuplem4  42474  smflimsuplem5  42475  smflimsuplem7  42477  smfliminflem  42481  ralndv2  42657  iccelpart  42911  eliunxp2  43686