Theorem rgenw 3083

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

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

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

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

This theorem is used by:  rgen2w  3084  reuss  4274  reuun1  4275  rabnc  4343  riinrab  5046  0disj  5098  iinexg  5312  epse  5636  xpiindi  5816  eliunxp  5818  opeliunxp2  5819  elrnmpti  5948  cnviin  6295  fnmpti  6690  eqfnfv  7037  eufnfv  7242  mpoeq12  7500  porpss  7750  iunex  7987  abrexex2  7988  mpoex  8100  suppssov1  8225  suppssov2  8226  suppssfv  8230  opeliunxp2f  8238  onnseq  8363  ixpssmap  8971  boxcutc  8980  nneneq  9232  finsschain  9359  dfom3  9658  cantnfdm  9675  rankuni2b  9877  rankval4b  9890  rankval4  9894  rankfilimbi  9912  alephf1  10174  dfac4  10211  dfacacn  10230  infmap2  10305  cfeq0  10344  fin23lem28  10428  axdc2lem  10536  axcclem  10545  ac6  10568  iundom  10636  konigthlem  10663  iunctb  10669  tskmid  10935  supaddc  12294  supadd  12295  supmul1  12296  supmullem2  12298  supmul  12299  uzf  12978  seqof  14212  hashbclem  14607  rlimclim1  15724  fsumcom2  15952  ackbijnn  16009  fprodcom2  16163  lcmf0  16821  phisum  16980  sumhash  17086  ramcl  17219  prdsvallem  17637  prdsval  17638  prdsbas  17640  prdshom  17650  imasplusg  17701  imasmulr  17702  imasvsca  17704  imasip  17705  imasaddfnlem  17712  imasvscafn  17721  isfunc  18051  wunfunc  18088  isnat  18137  natffn  18139  wunnat  18146  fucsect  18162  setcepi  18275  grpinvfval  19201  odfval  19758  dfod2  19790  ghmcyg  20122  gsum2d2lem  20199  gsum2d2  20200  gsumcom2  20201  dmdprd  20226  dprdval  20231  dprdf11  20251  dprd2d2  20272  dpjeq  20287  pgpfac1lem2  20303  pgpfac1lem3  20305  pgpfac1lem4  20306  mptscmfsupp0  21214  00lsp  21268  ocv0  21995  ofco2  22778  matunitlindflem1  23006  tgidm  23310  pptbas  23338  tgrest  23489  iscnp2  23569  ist1-3  23679  discmp  23728  1stcfb  23775  lly1stc  23827  disllycmp  23829  dis1stc  23830  comppfsc  23863  txbas  23898  ptbasfi  23912  ptpjopn  23943  dfac14  23949  ptrescn  23970  xkoptsub  23985  fclsval  24339  ptcmplem2  24384  ptcmplem3  24385  cnextrel  24394  tsmsfbas  24459  ustuqtop  24577  prdsxmetlem  24699  ressprdsds  24702  prdsxmslem2  24860  zcld  25145  xrge0tsms  25166  metdsf  25180  metdsge  25181  minveclem1  25757  minveclem3b  25761  minveclem6  25767  uniioombllem4  25919  uniioombllem6  25921  ismbf3d  25987  i1f1lem  26022  reldv  26202  ellimc2  26209  limcflf  26213  limciun  26226  dvfval  26229  dvrec  26287  dvlipcn  26326  mdegle0  26407  ply1nzb  26453  quotlem  26633  taylfval  26698  ulmdvlem1  26739  ulmdvlem2  26740  ulmdvlem3  26741  psercn  26765  sqff1o  27521  lgsquadlem2  27720  bdayiun  28313  disjxwwlksn  30505  disjxwwlkn  30514  numclwwlk3lem2  30997  grpoidval  31127  grpoidinv2  31129  grpoinv  31139  minvecolem1  31488  minvecolem5  31495  minvecolem6  31496  adjbdln  32697  dfcnv2  33323  intimafv  33358  rexdiv  33545  gsumpart  33677  xrge0tsmsd  33687  fedgmullem2  34315  irngval  34370  rspectopn  34552  zarcls  34559  zartopn  34560  esumnul  34733  esum0  34734  hasheuni  34770  esum2d  34778  ldgenpisyslem3  34851  measvuni  34900  measdivcstALTV  34911  ddemeas  34922  carsgclctunlem2  35004  eulerpartlemgs2  35065  probfinmeasbALTV  35114  0rrv  35136  signsplypnf  35232  signsply0  35233  hgt750lemb  35338  bnj226  35418  bnj98  35550  bnj517  35568  bnj893  35611  bnj1137  35678  soinfdom  35777  rankse  35802  fineqvnttrclse  35863  tz9.1regs  35873  onprcf1acwevdlem2  36000  vsmrep  36044  subfacf  36061  subfacp1lem6  36071  cvmsss2  36160  cvmliftlem1  36171  nmulr0  37071  ixpeq12i  37117  ttciunun  37426  bj-rabtr  37970  bj-axseprep  38129  relowlssretop  38426  fin2so  38670  ptrest  38677  poimirlem23  38701  poimirlem24  38702  poimirlem27  38705  poimirlem30  38708  poimirlem32  38710  cnambfre  38726  upixp  38803  0totbnd  38847  prdsbnd  38867  prdstotbnd  38868  cntotbnd  38870  rrnequiv  38909  ac6s6  39244  dmsucmap  39540  disjimeceqim  39876  cdlemefrs32fva  41597  cdlemkid5  42132  cdlemk56  42168  dihf11lem  42463  addinvcom  43623  0dioph  43929  vdioph  43930  pw2f1ocnv  44184  pwinfi  44705  eliunov2  44819  fvmptiunrelexplb0d  44824  fvmptiunrelexplb1d  44826  iunrelexp0  44842  ntrrn  45262  dssmapntrcls  45268  mnurndlem1  45405  rankrelp  46089  0elaxnul  46112  prclaxpr  46114  uniclaxun  46115  omssaxinf2  46117  wessf1ornlem  46339  axccdom  46374  fnmptif  46416  fsumiunss  46726  limcdm0  46769  liminfval2  46917  liminflelimsuplem  46924  cnrefiisplem  46978  0cnf  47026  dvsinax  47062  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnprodlem3  47097  iblempty  47114  fourierdlem89  47344  fourierdlem91  47346  fourierdlem100  47355  fourierdlem108  47363  fourierdlem112  47367  salexct3  47491  salgensscntex  47493  omeiunle  47666  0ome  47678  hoissrrn  47698  ovn0  47715  hoissrrn2  47727  hspmbl  47778  ovolval5lem2  47802  iunhoiioolem  47824  vonioolem2  47830  vonicclem2  47833  smflimlem1  47920  smfsuplem1  47960  smfinflem  47966  smflimsuplem1  47969  smflimsuplem2  47970  smflimsuplem3  47971  smflimsuplem4  47972  smflimsuplem5  47973  smflimsuplem7  47975  smfliminflem  47979  sqrtnnaa  48052  sqrtnzqaa  48053  sqrtnpoly  48082  ralndv2  48316  iccelpart  48654  eliunxp2  49585  1arymaptf1  49893  iinxp  50081  iinfssclem2  50308  iinfssclem3  50309  iinfssc  50310  imasubclem1  50359