Theorem rgenw 3084

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

This proof depends on syntax axioms:   ∈ wcel 2147  ∀wral 3080

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 3081

This theorem is used by:  rgen2w  3085  reuss  4275  reuun1  4276  rabnc  4344  riinrab  5049  0disj  5101  iinexg  5316  epse  5640  xpiindi  5822  eliunxp  5824  opeliunxp2  5825  elrnmpti  5956  cnviin  6313  fnmpti  6712  eqfnfv  7060  eufnfv  7266  mpoeq12  7524  porpss  7775  iunex  8014  abrexex2  8015  mpoex  8127  suppssov1  8252  suppssov2  8253  suppssfv  8257  opeliunxp2f  8265  onnseq  8390  ixpssmap  8998  boxcutc  9007  nneneq  9259  finsschain  9386  dfom3  9685  cantnfdm  9702  rankuni2b  9904  rankval4b  9917  rankval4  9921  rankfilimbi  9939  alephf1  10203  dfac4  10240  dfacacn  10259  infmap2  10334  cfeq0  10373  fin23lem28  10457  axdc2lem  10565  axcclem  10574  ac6  10597  iundom  10665  konigthlem  10692  iunctb  10698  tskmid  10964  supaddc  12324  supadd  12325  supmul1  12326  supmullem2  12328  supmul  12329  uzf  13008  seqof  14242  hashbclem  14638  rlimclim1  15756  fsumcom2  15984  ackbijnn  16041  fprodcom2  16195  lcmf0  16853  phisum  17012  sumhash  17118  ramcl  17251  prdsvallem  17675  prdsval  17676  prdsbas  17678  prdshom  17688  imasplusg  17739  imasmulr  17740  imasvsca  17742  imasip  17743  imasaddfnlem  17750  imasvscafn  17759  isfunc  18089  wunfunc  18126  isnat  18175  natffn  18177  wunnat  18184  fucsect  18200  setcepi  18313  grpinvfval  19239  odfval  19797  dfod2  19829  ghmcyg  20161  gsum2d2lem  20238  gsum2d2  20239  gsumcom2  20240  dmdprd  20265  dprdval  20270  dprdf11  20290  dprd2d2  20311  dpjeq  20326  pgpfac1lem2  20342  pgpfac1lem3  20344  pgpfac1lem4  20345  mptscmfsupp0  21253  00lsp  21307  ocv0  22038  ofco2  22821  matunitlindflem1  23049  tgidm  23353  pptbas  23381  tgrest  23532  iscnp2  23612  ist1-3  23722  discmp  23771  1stcfb  23818  lly1stc  23870  disllycmp  23872  dis1stc  23873  comppfsc  23906  txbas  23941  ptbasfi  23955  ptpjopn  23986  dfac14  23992  ptrescn  24013  xkoptsub  24028  fclsval  24382  ptcmplem2  24427  ptcmplem3  24428  cnextrel  24437  tsmsfbas  24502  ustuqtop  24620  prdsxmetlem  24742  ressprdsds  24745  prdsxmslem2  24903  zcld  25188  xrge0tsms  25209  metdsf  25223  metdsge  25224  minveclem1  25800  minveclem3b  25804  minveclem6  25810  uniioombllem4  25962  uniioombllem6  25964  ismbf3d  26030  i1f1lem  26065  reldv  26245  ellimc2  26252  limcflf  26256  limciun  26269  dvfval  26272  dvrec  26330  dvlipcn  26369  mdegle0  26450  ply1nzb  26496  quotlem  26676  taylfval  26743  ulmdvlem1  26784  ulmdvlem2  26785  ulmdvlem3  26786  psercn  26810  sqff1o  27566  lgsquadlem2  27765  bdayiun  28358  disjxwwlksn  30550  disjxwwlkn  30559  numclwwlk3lem2  31042  grpoidval  31172  grpoidinv2  31174  grpoinv  31184  minvecolem1  31533  minvecolem5  31540  minvecolem6  31541  adjbdln  32742  dfcnv2  33366  intimafv  33401  rexdiv  33588  gsumpart  33723  xrge0tsmsd  33733  fedgmullem2  34373  irngval  34428  rspectopn  34610  zarcls  34617  zartopn  34618  esumnul  34791  esum0  34792  hasheuni  34828  esum2d  34836  ldgenpisyslem3  34909  measvuni  34958  measdivcstALTV  34969  ddemeas  34980  carsgclctunlem2  35062  eulerpartlemgs2  35123  probfinmeasbALTV  35172  0rrv  35194  signsplypnf  35290  signsply0  35291  hgt750lemb  35396  bnj226  35476  bnj98  35608  bnj517  35626  bnj893  35669  bnj1137  35736  soinfdom  35841  rankse  35864  fineqvnttrclse  35933  tz9.1regs  35943  onprcf1acwevdlem2  36087  vsmrep  36131  subfacf  36148  subfacp1lem6  36158  cvmsss2  36247  cvmliftlem1  36258  nmulr0  37159  ixpeq12i  37205  ttciunun  37514  bj-rabtr  38058  bj-axseprep  38260  relowlssretop  38554  fin2so  38798  ptrest  38805  poimirlem23  38829  poimirlem24  38830  poimirlem27  38833  poimirlem30  38836  poimirlem32  38838  cnambfre  38854  upixp  38931  0totbnd  38973  prdsbnd  38993  prdstotbnd  38994  cntotbnd  38996  rrnequiv  39035  ac6s6  39370  dmsucmap  39666  disjimeceqim  40002  cdlemefrs32fva  41723  cdlemkid5  42258  cdlemk56  42294  dihf11lem  42589  addinvcom  43749  0dioph  44055  vdioph  44056  pw2f1ocnv  44310  pwinfi  44826  eliunov2  44940  fvmptiunrelexplb0d  44945  fvmptiunrelexplb1d  44947  iunrelexp0  44963  ntrrn  45383  dssmapntrcls  45389  mnurndlem1  45526  rankrelp  46214  0elaxnul  46237  prclaxpr  46239  uniclaxun  46240  omssaxinf2  46242  wessf1ornlem  46473  axccdom  46508  fnmptif  46550  fsumiunss  46860  limcdm0  46903  liminfval2  47051  liminflelimsuplem  47058  cnrefiisplem  47112  0cnf  47160  dvsinax  47196  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnprodlem3  47231  iblempty  47248  fourierdlem89  47478  fourierdlem91  47480  fourierdlem100  47489  fourierdlem108  47497  fourierdlem112  47501  salexct3  47625  salgensscntex  47627  omeiunle  47800  0ome  47812  hoissrrn  47832  ovn0  47849  hoissrrn2  47861  hspmbl  47912  ovolval5lem2  47936  iunhoiioolem  47958  vonioolem2  47964  vonicclem2  47967  smflimlem1  48054  smfsuplem1  48094  smfinflem  48100  smflimsuplem1  48103  smflimsuplem2  48104  smflimsuplem3  48105  smflimsuplem4  48106  smflimsuplem5  48107  smflimsuplem7  48109  smfliminflem  48113  sqrtnnaa  48186  sqrtnzqaa  48187  sqrtnpoly  48216  ralndv2  48450  iccelpart  48788  eliunxp2  49777  1arymaptf1  50085  iinxp  50273  iinfssclem2  50500  iinfssclem3  50501  iinfssc  50502  imasubclem1  50551