Theorem rgenw 3062

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

Syntax hints:   ∈ wcel 2105  ∀wral 3058

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

This theorem depends on definitions:  df-bi 207  df-ral 3059

This theorem is referenced by:  rgen2w  3063  reuss  4332  reuun1  4333  rabnc  4396  riinrab  5088  0disj  5140  iinexg  5353  epse  5670  xpiindi  5848  eliunxp  5850  opeliunxp2  5851  elrnmpti  5975  cnviin  6307  fnmpti  6711  eqfnfv  7050  eufnfv  7248  mpoeq12  7505  porpss  7745  iunex  7991  abrexex2  7992  mpoex  8102  suppssov1  8220  suppssov2  8221  suppssfv  8225  opeliunxp2f  8233  onnseq  8382  ixpssmap  8970  boxcutc  8979  nneneq  9243  nneneqOLD  9255  finsschain  9396  dfom3  9684  cantnfdm  9701  rankuni2b  9890  rankval4  9904  alephf1  10122  dfac4  10159  dfacacn  10179  infmap2  10254  cfeq0  10293  fin23lem28  10377  axdc2lem  10485  axcclem  10494  ac6  10517  iundom  10579  konigthlem  10605  iunctb  10611  tskmid  10877  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  supmul  12237  uzf  12878  seqof  14096  hashbclem  14487  rlimclim1  15577  fsumcom2  15806  ackbijnn  15860  fprodcom2  16016  lcmf0  16667  phisum  16823  sumhash  16929  ramcl  17062  prdsvallem  17500  prdsval  17501  prdsbas  17503  prdshom  17513  imasplusg  17563  imasmulr  17564  imasvsca  17566  imasip  17567  imasaddfnlem  17574  imasvscafn  17583  isfunc  17914  wunfunc  17951  wunfuncOLD  17952  isnat  18001  natffn  18003  wunnat  18010  wunnatOLD  18011  fucsect  18028  setcepi  18141  grpinvfval  19008  odfval  19564  dfod2  19596  ghmcyg  19928  gsum2d2lem  20005  gsum2d2  20006  gsumcom2  20007  dmdprd  20032  dprdval  20037  dprdf11  20057  dprd2d2  20078  dpjeq  20093  pgpfac1lem2  20109  pgpfac1lem3  20111  pgpfac1lem4  20112  mptscmfsupp0  20941  00lsp  20996  ocv0  21712  ofco2  22472  tgidm  23002  pptbas  23030  tgrest  23182  iscnp2  23262  ist1-3  23372  discmp  23421  1stcfb  23468  lly1stc  23519  disllycmp  23521  dis1stc  23522  comppfsc  23555  txbas  23590  ptbasfi  23604  ptpjopn  23635  dfac14  23641  ptrescn  23662  xkoptsub  23677  fclsval  24031  ptcmplem2  24076  ptcmplem3  24077  cnextrel  24086  tsmsfbas  24151  ustuqtop  24270  prdsxmetlem  24393  ressprdsds  24396  prdsxmslem2  24557  zcld  24848  xrge0tsms  24869  metdsf  24883  metdsge  24884  minveclem1  25471  minveclem3b  25475  minveclem6  25481  uniioombllem4  25634  uniioombllem6  25636  ismbf3d  25702  i1f1lem  25737  reldv  25919  ellimc2  25926  limcflf  25930  limciun  25943  dvfval  25946  dvrec  26007  dvlipcn  26047  mdegle0  26130  ply1nzb  26176  quotlem  26356  taylfval  26414  ulmdvlem1  26457  ulmdvlem2  26458  ulmdvlem3  26459  psercn  26484  sqff1o  27239  lgsquadlem2  27439  disjxwwlksn  29933  disjxwwlkn  29942  numclwwlk3lem2  30412  grpoidval  30541  grpoidinv2  30543  grpoinv  30553  minvecolem1  30902  minvecolem5  30909  minvecolem6  30910  adjbdln  32111  dfcnv2  32692  intimafv  32725  rexdiv  32892  gsumpart  33042  xrge0tsmsd  33047  fedgmullem2  33657  irngval  33699  rspectopn  33827  zarcls  33834  zartopn  33835  esumnul  34028  esum0  34029  hasheuni  34065  esum2d  34073  ldgenpisyslem3  34145  measvuni  34194  measdivcstALTV  34205  ddemeas  34216  carsgclctunlem2  34300  eulerpartlemgs2  34361  probfinmeasbALTV  34410  0rrv  34432  signsplypnf  34543  signsply0  34544  hgt750lemb  34649  bnj226  34726  bnj98  34859  bnj517  34877  bnj893  34920  bnj1137  34987  subfacf  35159  subfacp1lem6  35169  cvmsss2  35258  cvmliftlem1  35269  ixpeq12i  36182  bj-rabtr  36912  relowlssretop  37345  fin2so  37593  matunitlindflem1  37602  ptrest  37605  poimirlem23  37629  poimirlem24  37630  poimirlem27  37633  poimirlem30  37636  poimirlem32  37638  cnambfre  37654  upixp  37715  0totbnd  37759  prdsbnd  37779  prdstotbnd  37780  cntotbnd  37782  rrnequiv  37821  ac6s6  38158  cdlemefrs32fva  40382  cdlemkid5  40917  cdlemk56  40953  dihf11lem  41248  addinvcom  42437  0dioph  42765  vdioph  42766  rmxyelqirrOLD  42898  pw2f1ocnv  43025  pwinfi  43553  eliunov2  43668  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  iunrelexp0  43691  ntrrn  44111  dssmapntrcls  44117  mnurndlem1  44276  prclaxpr  44947  wessf1ornlem  45127  axccdom  45164  mpteq1dfOLD  45179  fnmptif  45210  fsumiunss  45530  limcdm0  45573  liminfval2  45723  liminflelimsuplem  45730  cnrefiisplem  45784  0cnf  45832  dvsinax  45868  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem3  45903  iblempty  45920  fourierdlem89  46150  fourierdlem91  46152  fourierdlem100  46161  fourierdlem108  46169  fourierdlem112  46173  salexct3  46297  salgensscntex  46299  omeiunle  46472  0ome  46484  hoissrrn  46504  ovn0  46521  hoissrrn2  46533  hspmbl  46584  ovolval5lem2  46608  iunhoiioolem  46630  vonioolem2  46636  vonicclem2  46639  smflimlem1  46726  smfsuplem1  46766  smfinflem  46772  smflimsuplem1  46775  smflimsuplem2  46776  smflimsuplem3  46777  smflimsuplem4  46778  smflimsuplem5  46779  smflimsuplem7  46781  smfliminflem  46785  ralndv2  47055  iccelpart  47357  eliunxp2  48178  1arymaptf1  48491