Theorem rgenw 3081

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

This proof depends on syntax axioms:   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  rgen2w  3082  reuss  4273  reuun1  4274  rabnc  4341  riinrab  5044  0disj  5096  iinexg  5309  epse  5633  xpiindi  5812  eliunxp  5814  opeliunxp2  5815  elrnmpti  5944  cnviin  6289  fnmpti  6682  eqfnfv  7029  eufnfv  7235  mpoeq12  7493  porpss  7743  iunex  7980  abrexex2  7981  mpoex  8092  suppssov1  8214  suppssov2  8215  suppssfv  8219  opeliunxp2f  8227  onnseq  8352  ixpssmap  8960  boxcutc  8969  nneneq  9221  finsschain  9348  dfom3  9648  cantnfdm  9665  rankuni2b  9867  rankval4b  9880  rankval4  9884  rankfilimbi  9902  alephf1  10164  dfac4  10201  dfacacn  10220  infmap2  10295  cfeq0  10334  fin23lem28  10418  axdc2lem  10526  axcclem  10535  ac6  10558  iundom  10626  konigthlem  10653  iunctb  10659  tskmid  10925  supaddc  12284  supadd  12285  supmul1  12286  supmullem2  12288  supmul  12289  uzf  12968  seqof  14202  hashbclem  14597  rlimclim1  15712  fsumcom2  15940  ackbijnn  15997  fprodcom2  16151  lcmf0  16809  phisum  16968  sumhash  17074  ramcl  17207  prdsvallem  17625  prdsval  17626  prdsbas  17628  prdshom  17638  imasplusg  17689  imasmulr  17690  imasvsca  17692  imasip  17693  imasaddfnlem  17700  imasvscafn  17709  isfunc  18039  wunfunc  18076  isnat  18125  natffn  18127  wunnat  18134  fucsect  18150  setcepi  18263  grpinvfval  19189  odfval  19746  dfod2  19778  ghmcyg  20110  gsum2d2lem  20187  gsum2d2  20188  gsumcom2  20189  dmdprd  20214  dprdval  20219  dprdf11  20239  dprd2d2  20260  dpjeq  20275  pgpfac1lem2  20291  pgpfac1lem3  20293  pgpfac1lem4  20294  mptscmfsupp0  21202  00lsp  21256  ocv0  21983  ofco2  22766  matunitlindflem1  22994  tgidm  23298  pptbas  23326  tgrest  23477  iscnp2  23557  ist1-3  23667  discmp  23716  1stcfb  23763  lly1stc  23815  disllycmp  23817  dis1stc  23818  comppfsc  23851  txbas  23886  ptbasfi  23900  ptpjopn  23931  dfac14  23937  ptrescn  23958  xkoptsub  23973  fclsval  24327  ptcmplem2  24372  ptcmplem3  24373  cnextrel  24382  tsmsfbas  24447  ustuqtop  24565  prdsxmetlem  24687  ressprdsds  24690  prdsxmslem2  24848  zcld  25133  xrge0tsms  25154  metdsf  25168  metdsge  25169  minveclem1  25745  minveclem3b  25749  minveclem6  25755  uniioombllem4  25907  uniioombllem6  25909  ismbf3d  25975  i1f1lem  26010  reldv  26190  ellimc2  26197  limcflf  26201  limciun  26214  dvfval  26217  dvrec  26275  dvlipcn  26314  mdegle0  26395  ply1nzb  26441  quotlem  26621  taylfval  26686  ulmdvlem1  26727  ulmdvlem2  26728  ulmdvlem3  26729  psercn  26753  sqff1o  27509  lgsquadlem2  27708  bdayiun  28301  disjxwwlksn  30493  disjxwwlkn  30502  numclwwlk3lem2  30985  grpoidval  31115  grpoidinv2  31117  grpoinv  31127  minvecolem1  31476  minvecolem5  31483  minvecolem6  31484  adjbdln  32685  dfcnv2  33269  intimafv  33304  rexdiv  33492  gsumpart  33624  xrge0tsmsd  33634  fedgmullem2  34262  irngval  34317  rspectopn  34499  zarcls  34506  zartopn  34507  esumnul  34680  esum0  34681  hasheuni  34717  esum2d  34725  ldgenpisyslem3  34798  measvuni  34847  measdivcstALTV  34858  ddemeas  34869  carsgclctunlem2  34951  eulerpartlemgs2  35012  probfinmeasbALTV  35061  0rrv  35083  signsplypnf  35179  signsply0  35180  hgt750lemb  35285  bnj226  35365  bnj98  35497  bnj517  35515  bnj893  35558  bnj1137  35625  soinfdom  35717  fineqvnttrclse  35792  tz9.1regs  35802  onprcf1acwevdlem2  35896  subfacf  35940  subfacp1lem6  35950  cvmsss2  36039  cvmliftlem1  36050  nmulr0  36944  ixpeq12i  36990  ttciunun  37299  bj-rabtr  37843  bj-axseprep  37990  relowlssretop  38286  fin2so  38530  ptrest  38537  poimirlem23  38561  poimirlem24  38562  poimirlem27  38565  poimirlem30  38568  poimirlem32  38570  cnambfre  38586  upixp  38663  0totbnd  38707  prdsbnd  38727  prdstotbnd  38728  cntotbnd  38730  rrnequiv  38769  ac6s6  39104  dmsucmap  39400  disjimeceqim  39736  cdlemefrs32fva  41457  cdlemkid5  41992  cdlemk56  42028  dihf11lem  42323  addinvcom  43483  0dioph  43788  vdioph  43789  pw2f1ocnv  44043  pwinfi  44564  eliunov2  44678  fvmptiunrelexplb0d  44683  fvmptiunrelexplb1d  44685  iunrelexp0  44701  ntrrn  45121  dssmapntrcls  45127  mnurndlem1  45264  rankrelp  45949  0elaxnul  45972  prclaxpr  45974  uniclaxun  45975  omssaxinf2  45977  wessf1ornlem  46199  axccdom  46234  fnmptif  46276  fsumiunss  46586  limcdm0  46629  liminfval2  46777  liminflelimsuplem  46784  cnrefiisplem  46838  0cnf  46886  dvsinax  46922  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem3  46957  iblempty  46974  fourierdlem89  47204  fourierdlem91  47206  fourierdlem100  47215  fourierdlem108  47223  fourierdlem112  47227  salexct3  47351  salgensscntex  47353  omeiunle  47526  0ome  47538  hoissrrn  47558  ovn0  47575  hoissrrn2  47587  hspmbl  47638  ovolval5lem2  47662  iunhoiioolem  47684  vonioolem2  47690  vonicclem2  47693  smflimlem1  47780  smfsuplem1  47820  smfinflem  47826  smflimsuplem1  47829  smflimsuplem2  47830  smflimsuplem3  47831  smflimsuplem4  47832  smflimsuplem5  47833  smflimsuplem7  47835  smfliminflem  47839  sqrtnnaa  47912  sqrtnzqaa  47913  sqrtnpoly  47942  ralndv2  48175  iccelpart  48514  eliunxp2  49445  1arymaptf1  49753  iinxp  49940  iinfssclem2  50162  iinfssclem3  50163  iinfssc  50164  imasubclem1  50211