Theorem rgenw 3085

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

This proof depends on syntax axioms:   ∈ wcel 2146  ∀wral 3081

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 3082

This theorem is used by:  rgen2w  3086  reuss  4280  reuun1  4281  rabnc  4348  riinrab  5052  0disj  5104  iinexg  5320  epse  5645  xpiindi  5823  eliunxp  5825  opeliunxp2  5826  elrnmpti  5954  cnviin  6291  fnmpti  6682  eqfnfv  7029  eufnfv  7234  mpoeq12  7492  porpss  7734  iunex  7971  abrexex2  7972  mpoex  8082  suppssov1  8199  suppssov2  8200  suppssfv  8204  opeliunxp2f  8212  onnseq  8337  ixpssmap  8936  boxcutc  8945  nneneq  9197  finsschain  9323  dfom3  9623  cantnfdm  9640  rankuni2b  9832  rankval4  9846  alephf1  10085  dfac4  10122  dfacacn  10141  infmap2  10216  cfeq0  10255  fin23lem28  10339  axdc2lem  10447  axcclem  10456  ac6  10479  iundom  10543  konigthlem  10570  iunctb  10576  tskmid  10842  supaddc  12199  supadd  12200  supmul1  12201  supmullem2  12203  supmul  12204  uzf  12883  seqof  14115  hashbclem  14509  rlimclim1  15622  fsumcom2  15850  ackbijnn  15907  fprodcom2  16063  lcmf0  16716  phisum  16874  sumhash  16980  ramcl  17113  prdsvallem  17531  prdsval  17532  prdsbas  17534  prdshom  17544  imasplusg  17595  imasmulr  17596  imasvsca  17598  imasip  17599  imasaddfnlem  17606  imasvscafn  17615  isfunc  17945  wunfunc  17982  isnat  18031  natffn  18033  wunnat  18040  fucsect  18056  setcepi  18169  grpinvfval  19091  odfval  19648  dfod2  19680  ghmcyg  20012  gsum2d2lem  20089  gsum2d2  20090  gsumcom2  20091  dmdprd  20116  dprdval  20121  dprdf11  20141  dprd2d2  20162  dpjeq  20177  pgpfac1lem2  20193  pgpfac1lem3  20195  pgpfac1lem4  20196  mptscmfsupp0  21100  00lsp  21154  ocv0  21879  ofco2  22660  tgidm  23189  pptbas  23217  tgrest  23368  iscnp2  23448  ist1-3  23558  discmp  23607  1stcfb  23654  lly1stc  23706  disllycmp  23708  dis1stc  23709  comppfsc  23742  txbas  23777  ptbasfi  23791  ptpjopn  23822  dfac14  23828  ptrescn  23849  xkoptsub  23864  fclsval  24218  ptcmplem2  24263  ptcmplem3  24264  cnextrel  24273  tsmsfbas  24338  ustuqtop  24456  prdsxmetlem  24578  ressprdsds  24581  prdsxmslem2  24739  zcld  25024  xrge0tsms  25045  metdsf  25059  metdsge  25060  minveclem1  25636  minveclem3b  25640  minveclem6  25646  uniioombllem4  25798  uniioombllem6  25800  ismbf3d  25866  i1f1lem  25901  reldv  26082  ellimc2  26089  limcflf  26093  limciun  26106  dvfval  26109  dvrec  26167  dvlipcn  26206  mdegle0  26287  ply1nzb  26333  quotlem  26514  taylfval  26575  ulmdvlem1  26616  ulmdvlem2  26617  ulmdvlem3  26618  psercn  26642  sqff1o  27399  lgsquadlem2  27598  bdayiun  28161  disjxwwlksn  30322  disjxwwlkn  30331  numclwwlk3lem2  30808  grpoidval  30938  grpoidinv2  30940  grpoinv  30950  minvecolem1  31299  minvecolem5  31306  minvecolem6  31307  adjbdln  32508  dfcnv2  33093  intimafv  33129  rexdiv  33317  gsumpart  33449  xrge0tsmsd  33459  fedgmullem2  34086  irngval  34141  rspectopn  34323  zarcls  34330  zartopn  34331  esumnul  34504  esum0  34505  hasheuni  34541  esum2d  34549  ldgenpisyslem3  34622  measvuni  34671  measdivcstALTV  34682  ddemeas  34693  carsgclctunlem2  34776  eulerpartlemgs2  34837  probfinmeasbALTV  34886  0rrv  34908  signsplypnf  35004  signsply0  35005  hgt750lemb  35110  bnj226  35190  bnj98  35322  bnj517  35340  bnj893  35383  bnj1137  35450  rankval4b  35553  rankfilimbi  35555  fineqvnttrclse  35596  tz9.1regs  35606  subfacf  35706  subfacp1lem6  35716  cvmsss2  35805  cvmliftlem1  35816  nmulr0  36726  ixpeq12i  36772  ttciunun  37081  bj-rabtr  37625  bj-axseprep  37770  relowlssretop  38068  fin2so  38317  matunitlindflem1  38326  ptrest  38329  poimirlem23  38353  poimirlem24  38354  poimirlem27  38357  poimirlem30  38360  poimirlem32  38362  cnambfre  38378  upixp  38440  0totbnd  38484  prdsbnd  38504  prdstotbnd  38505  cntotbnd  38507  rrnequiv  38546  ac6s6  38881  dmsucmap  39177  disjimeceqim  39513  cdlemefrs32fva  41234  cdlemkid5  41769  cdlemk56  41805  dihf11lem  42100  addinvcom  43253  0dioph  43569  vdioph  43570  pw2f1ocnv  43824  pwinfi  44350  eliunov2  44465  fvmptiunrelexplb0d  44470  fvmptiunrelexplb1d  44472  iunrelexp0  44488  ntrrn  44908  dssmapntrcls  44914  mnurndlem1  45051  rankrelp  45729  0elaxnul  45752  prclaxpr  45754  uniclaxun  45755  omssaxinf2  45757  wessf1ornlem  45963  axccdom  45998  fnmptif  46040  fsumiunss  46351  limcdm0  46394  liminfval2  46542  liminflelimsuplem  46549  cnrefiisplem  46603  0cnf  46651  dvsinax  46687  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnprodlem3  46722  iblempty  46739  fourierdlem89  46969  fourierdlem91  46971  fourierdlem100  46980  fourierdlem108  46988  fourierdlem112  46992  salexct3  47116  salgensscntex  47118  omeiunle  47291  0ome  47303  hoissrrn  47323  ovn0  47340  hoissrrn2  47352  hspmbl  47403  ovolval5lem2  47427  iunhoiioolem  47449  vonioolem2  47455  vonicclem2  47458  smflimlem1  47545  smfsuplem1  47585  smfinflem  47591  smflimsuplem1  47594  smflimsuplem2  47595  smflimsuplem3  47596  smflimsuplem4  47597  smflimsuplem5  47598  smflimsuplem7  47600  smfliminflem  47604  sqrtnnaa  47664  sqrtnzqaa  47665  ralndv2  47903  iccelpart  48242  eliunxp2  49173  1arymaptf1  49481  iinxp  49668  iinfssclem2  49892  iinfssclem3  49893  iinfssc  49894  imasubclem1  49941