Theorem rgenw 3080

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

This proof depends on syntax axioms:   ∈ wcel 2145  ∀wral 3076

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 3077

This theorem is used by:  rgen2w  3081  reuss  4273  reuun1  4274  rabnc  4341  riinrab  5044  0disj  5096  iinexg  5312  epse  5637  xpiindi  5815  eliunxp  5817  opeliunxp2  5818  elrnmpti  5946  cnviin  6284  fnmpti  6676  eqfnfv  7023  eufnfv  7229  mpoeq12  7487  porpss  7729  iunex  7966  abrexex2  7967  mpoex  8079  suppssov1  8196  suppssov2  8197  suppssfv  8201  opeliunxp2f  8209  onnseq  8334  ixpssmap  8940  boxcutc  8949  nneneq  9201  finsschain  9327  dfom3  9627  cantnfdm  9644  rankuni2b  9836  rankval4  9850  alephf1  10089  dfac4  10126  dfacacn  10145  infmap2  10220  cfeq0  10259  fin23lem28  10343  axdc2lem  10451  axcclem  10460  ac6  10483  iundom  10551  konigthlem  10578  iunctb  10584  tskmid  10850  supaddc  12207  supadd  12208  supmul1  12209  supmullem2  12211  supmul  12212  uzf  12891  seqof  14124  hashbclem  14518  rlimclim1  15633  fsumcom2  15861  ackbijnn  15918  fprodcom2  16072  lcmf0  16725  phisum  16883  sumhash  16989  ramcl  17122  prdsvallem  17540  prdsval  17541  prdsbas  17543  prdshom  17553  imasplusg  17604  imasmulr  17605  imasvsca  17607  imasip  17608  imasaddfnlem  17615  imasvscafn  17624  isfunc  17954  wunfunc  17991  isnat  18040  natffn  18042  wunnat  18049  fucsect  18065  setcepi  18178  grpinvfval  19103  odfval  19660  dfod2  19692  ghmcyg  20024  gsum2d2lem  20101  gsum2d2  20102  gsumcom2  20103  dmdprd  20128  dprdval  20133  dprdf11  20153  dprd2d2  20174  dpjeq  20189  pgpfac1lem2  20205  pgpfac1lem3  20207  pgpfac1lem4  20208  mptscmfsupp0  21112  00lsp  21166  ocv0  21891  ofco2  22674  matunitlindflem1  22902  tgidm  23206  pptbas  23234  tgrest  23385  iscnp2  23465  ist1-3  23575  discmp  23624  1stcfb  23671  lly1stc  23723  disllycmp  23725  dis1stc  23726  comppfsc  23759  txbas  23794  ptbasfi  23808  ptpjopn  23839  dfac14  23845  ptrescn  23866  xkoptsub  23881  fclsval  24235  ptcmplem2  24280  ptcmplem3  24281  cnextrel  24290  tsmsfbas  24355  ustuqtop  24473  prdsxmetlem  24595  ressprdsds  24598  prdsxmslem2  24756  zcld  25041  xrge0tsms  25062  metdsf  25076  metdsge  25077  minveclem1  25653  minveclem3b  25657  minveclem6  25663  uniioombllem4  25815  uniioombllem6  25817  ismbf3d  25883  i1f1lem  25918  reldv  26098  ellimc2  26105  limcflf  26109  limciun  26122  dvfval  26125  dvrec  26183  dvlipcn  26222  mdegle0  26303  ply1nzb  26349  quotlem  26531  taylfval  26596  ulmdvlem1  26637  ulmdvlem2  26638  ulmdvlem3  26639  psercn  26663  sqff1o  27419  lgsquadlem2  27618  bdayiun  28181  disjxwwlksn  30373  disjxwwlkn  30382  numclwwlk3lem2  30865  grpoidval  30995  grpoidinv2  30997  grpoinv  31007  minvecolem1  31356  minvecolem5  31363  minvecolem6  31364  adjbdln  32565  dfcnv2  33149  intimafv  33184  rexdiv  33372  gsumpart  33504  xrge0tsmsd  33514  fedgmullem2  34141  irngval  34196  rspectopn  34378  zarcls  34385  zartopn  34386  esumnul  34559  esum0  34560  hasheuni  34596  esum2d  34604  ldgenpisyslem3  34677  measvuni  34726  measdivcstALTV  34737  ddemeas  34748  carsgclctunlem2  34831  eulerpartlemgs2  34892  probfinmeasbALTV  34941  0rrv  34963  signsplypnf  35059  signsply0  35060  hgt750lemb  35165  bnj226  35245  bnj98  35377  bnj517  35395  bnj893  35438  bnj1137  35505  rankval4b  35608  rankfilimbi  35610  fineqvnttrclse  35651  tz9.1regs  35661  subfacf  35755  subfacp1lem6  35765  cvmsss2  35854  cvmliftlem1  35865  nmulr0  36776  ixpeq12i  36822  ttciunun  37131  bj-rabtr  37675  bj-axseprep  37820  relowlssretop  38118  fin2so  38362  ptrest  38369  poimirlem23  38393  poimirlem24  38394  poimirlem27  38397  poimirlem30  38400  poimirlem32  38402  cnambfre  38418  upixp  38480  0totbnd  38524  prdsbnd  38544  prdstotbnd  38545  cntotbnd  38547  rrnequiv  38586  ac6s6  38921  dmsucmap  39217  disjimeceqim  39553  cdlemefrs32fva  41274  cdlemkid5  41809  cdlemk56  41845  dihf11lem  42140  addinvcom  43308  0dioph  43624  vdioph  43625  pw2f1ocnv  43879  pwinfi  44405  eliunov2  44520  fvmptiunrelexplb0d  44525  fvmptiunrelexplb1d  44527  iunrelexp0  44543  ntrrn  44963  dssmapntrcls  44969  mnurndlem1  45106  rankrelp  45784  0elaxnul  45807  prclaxpr  45809  uniclaxun  45810  omssaxinf2  45812  wessf1ornlem  46018  axccdom  46053  fnmptif  46095  fsumiunss  46406  limcdm0  46449  liminfval2  46597  liminflelimsuplem  46604  cnrefiisplem  46658  0cnf  46706  dvsinax  46742  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnprodlem3  46777  iblempty  46794  fourierdlem89  47024  fourierdlem91  47026  fourierdlem100  47035  fourierdlem108  47043  fourierdlem112  47047  salexct3  47171  salgensscntex  47173  omeiunle  47346  0ome  47358  hoissrrn  47378  ovn0  47395  hoissrrn2  47407  hspmbl  47458  ovolval5lem2  47482  iunhoiioolem  47504  vonioolem2  47510  vonicclem2  47513  smflimlem1  47600  smfsuplem1  47640  smfinflem  47646  smflimsuplem1  47649  smflimsuplem2  47650  smflimsuplem3  47651  smflimsuplem4  47652  smflimsuplem5  47653  smflimsuplem7  47655  smfliminflem  47659  sqrtnnaa  47732  sqrtnzqaa  47733  sqrtnpoly  47762  ralndv2  47995  iccelpart  48334  eliunxp2  49265  1arymaptf1  49573  iinxp  49760  iinfssclem2  49982  iinfssclem3  49983  iinfssc  49984  imasubclem1  50031