Theorem rgenw 3057

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

Syntax hints:   ∈ wcel 2119  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  rgen2w  3058  reuss  4255  reuun1  4256  rabnc  4319  riinrab  5013  0disj  5065  iinexg  5276  epse  5600  xpiindi  5777  eliunxp  5779  opeliunxp2  5780  elrnmpti  5904  cnviin  6237  fnmpti  6628  eqfnfv  6971  eufnfv  7173  mpoeq12  7429  porpss  7670  iunex  7910  abrexex2  7911  mpoex  8021  suppssov1  8137  suppssov2  8138  suppssfv  8142  opeliunxp2f  8150  onnseq  8274  ixpssmap  8870  boxcutc  8879  nneneq  9130  finsschain  9259  dfom3  9559  cantnfdm  9576  rankuni2b  9768  rankval4  9782  alephf1  9998  dfac4  10035  dfacacn  10055  infmap2  10130  cfeq0  10169  fin23lem28  10253  axdc2lem  10361  axcclem  10370  ac6  10393  iundom  10455  konigthlem  10482  iunctb  10488  tskmid  10754  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  supmul  12119  uzf  12782  seqof  14012  hashbclem  14405  rlimclim1  15498  fsumcom2  15727  ackbijnn  15784  fprodcom2  15940  lcmf0  16594  phisum  16752  sumhash  16858  ramcl  16991  prdsvallem  17408  prdsval  17409  prdsbas  17411  prdshom  17421  imasplusg  17472  imasmulr  17473  imasvsca  17475  imasip  17476  imasaddfnlem  17483  imasvscafn  17492  isfunc  17822  wunfunc  17859  isnat  17908  natffn  17910  wunnat  17917  fucsect  17933  setcepi  18046  grpinvfval  18945  odfval  19498  dfod2  19530  ghmcyg  19862  gsum2d2lem  19939  gsum2d2  19940  gsumcom2  19941  dmdprd  19966  dprdval  19971  dprdf11  19991  dprd2d2  20012  dpjeq  20027  pgpfac1lem2  20043  pgpfac1lem3  20045  pgpfac1lem4  20046  mptscmfsupp0  20917  00lsp  20971  ocv0  21652  ofco2  22434  tgidm  22963  pptbas  22991  tgrest  23142  iscnp2  23222  ist1-3  23332  discmp  23381  1stcfb  23428  lly1stc  23479  disllycmp  23481  dis1stc  23482  comppfsc  23515  txbas  23550  ptbasfi  23564  ptpjopn  23595  dfac14  23601  ptrescn  23622  xkoptsub  23637  fclsval  23991  ptcmplem2  24036  ptcmplem3  24037  cnextrel  24046  tsmsfbas  24111  ustuqtop  24229  prdsxmetlem  24351  ressprdsds  24354  prdsxmslem2  24512  zcld  24797  xrge0tsms  24818  metdsf  24832  metdsge  24833  minveclem1  25409  minveclem3b  25413  minveclem6  25419  uniioombllem4  25571  uniioombllem6  25573  ismbf3d  25639  i1f1lem  25674  reldv  25855  ellimc2  25862  limcflf  25866  limciun  25879  dvfval  25882  dvrec  25940  dvlipcn  25979  mdegle0  26060  ply1nzb  26106  quotlem  26284  taylfval  26342  ulmdvlem1  26383  ulmdvlem2  26384  ulmdvlem3  26385  psercn  26409  sqff1o  27163  lgsquadlem2  27362  bdayiun  27925  disjxwwlksn  29990  disjxwwlkn  29999  numclwwlk3lem2  30472  grpoidval  30602  grpoidinv2  30604  grpoinv  30614  minvecolem1  30963  minvecolem5  30970  minvecolem6  30971  adjbdln  32172  dfcnv2  32767  intimafv  32803  rexdiv  33004  gsumpart  33144  xrge0tsmsd  33154  fedgmullem2  33814  irngval  33869  rspectopn  34051  zarcls  34058  zartopn  34059  esumnul  34232  esum0  34233  hasheuni  34269  esum2d  34277  ldgenpisyslem3  34349  measvuni  34398  measdivcstALTV  34409  ddemeas  34420  carsgclctunlem2  34503  eulerpartlemgs2  34564  probfinmeasbALTV  34613  0rrv  34635  signsplypnf  34734  signsply0  34735  hgt750lemb  34840  bnj226  34917  bnj98  35049  bnj517  35067  bnj893  35110  bnj1137  35177  rankval4b  35281  rankfilimbi  35282  fineqvnttrclse  35305  tz9.1regs  35315  subfacf  35403  subfacp1lem6  35413  cvmsss2  35502  cvmliftlem1  35513  ixpeq12i  36429  ttciunun  36739  bj-rabtr  37283  bj-axseprep  37427  relowlssretop  37725  fin2so  37974  matunitlindflem1  37983  ptrest  37986  poimirlem23  38010  poimirlem24  38011  poimirlem27  38014  poimirlem30  38017  poimirlem32  38019  cnambfre  38035  upixp  38096  0totbnd  38140  prdsbnd  38160  prdstotbnd  38161  cntotbnd  38163  rrnequiv  38202  ac6s6  38539  dmsucmap  38835  disjimeceqim  39171  cdlemefrs32fva  40892  cdlemkid5  41427  cdlemk56  41463  dihf11lem  41758  addinvcom  42909  0dioph  43227  vdioph  43228  pw2f1ocnv  43482  pwinfi  44008  eliunov2  44123  fvmptiunrelexplb0d  44128  fvmptiunrelexplb1d  44130  iunrelexp0  44146  ntrrn  44566  dssmapntrcls  44572  mnurndlem1  44725  rankrelp  45404  0elaxnul  45427  prclaxpr  45429  uniclaxun  45430  omssaxinf2  45432  wessf1ornlem  45632  axccdom  45667  fnmptif  45709  fsumiunss  46020  limcdm0  46063  liminfval2  46211  liminflelimsuplem  46218  cnrefiisplem  46272  0cnf  46320  dvsinax  46356  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnprodlem3  46391  iblempty  46408  fourierdlem89  46638  fourierdlem91  46640  fourierdlem100  46649  fourierdlem108  46657  fourierdlem112  46661  salexct3  46785  salgensscntex  46787  omeiunle  46960  0ome  46972  hoissrrn  46992  ovn0  47009  hoissrrn2  47021  hspmbl  47072  ovolval5lem2  47096  iunhoiioolem  47118  vonioolem2  47124  vonicclem2  47127  smflimlem1  47214  smfsuplem1  47254  smfinflem  47260  smflimsuplem1  47263  smflimsuplem2  47264  smflimsuplem3  47265  smflimsuplem4  47266  smflimsuplem5  47267  smflimsuplem7  47269  smfliminflem  47273  nthrucw  47331  ralndv2  47569  iccelpart  47908  eliunxp2  48825  1arymaptf1  49133  iinxp  49321  iinfssclem2  49545  iinfssclem3  49546  iinfssc  49547  imasubclem1  49594