Theorem rgenw 3066

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

Syntax hints:   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  rgen2w  3067  reuss  4316  reuun1  4317  rabnc  4387  riinrab  5087  0disj  5140  iinexg  5341  epse  5659  xpiindi  5834  eliunxp  5836  opeliunxp2  5837  elrnmpti  5958  cnviin  6283  fnmpti  6691  eqfnfv  7030  eufnfv  7228  mpoeq12  7479  porpss  7714  iunex  7952  abrexex2  7953  mpoex  8063  suppssov1  8180  suppssfv  8184  opeliunxp2f  8192  onnseq  8341  ixpssmap  8923  boxcutc  8932  nneneq  9206  nneneqOLD  9218  finsschain  9356  dfom3  9639  cantnfdm  9656  rankuni2b  9845  rankval4  9859  alephf1  10077  dfac4  10114  dfacacn  10133  infmap2  10210  cfeq0  10248  fin23lem28  10332  axdc2lem  10440  axcclem  10449  ac6  10472  iundom  10534  konigthlem  10560  iunctb  10566  tskmid  10832  supaddc  12178  supadd  12179  supmul1  12180  supmullem2  12182  supmul  12183  uzf  12822  seqof  14022  hashbclem  14408  rlimclim1  15486  fsumcom2  15717  ackbijnn  15771  fprodcom2  15925  lcmf0  16568  phisum  16720  sumhash  16826  ramcl  16959  prdsvallem  17397  prdsval  17398  prdsbas  17400  prdshom  17410  imasplusg  17460  imasmulr  17461  imasvsca  17463  imasip  17464  imasaddfnlem  17471  imasvscafn  17480  isfunc  17811  wunfunc  17846  wunfuncOLD  17847  isnat  17895  natffn  17897  wunnat  17904  wunnatOLD  17905  fucsect  17922  setcepi  18035  grpinvfval  18860  odfval  19395  dfod2  19427  ghmcyg  19759  gsum2d2lem  19836  gsum2d2  19837  gsumcom2  19838  dmdprd  19863  dprdval  19868  dprdf11  19888  dprd2d2  19909  dpjeq  19924  pgpfac1lem2  19940  pgpfac1lem3  19942  pgpfac1lem4  19943  mptscmfsupp0  20530  00lsp  20585  ocv0  21222  ofco2  21945  tgidm  22475  pptbas  22503  tgrest  22655  iscnp2  22735  ist1-3  22845  discmp  22894  1stcfb  22941  lly1stc  22992  disllycmp  22994  dis1stc  22995  comppfsc  23028  txbas  23063  ptbasfi  23077  ptpjopn  23108  dfac14  23114  ptrescn  23135  xkoptsub  23150  fclsval  23504  ptcmplem2  23549  ptcmplem3  23550  cnextrel  23559  tsmsfbas  23624  ustuqtop  23743  prdsxmetlem  23866  ressprdsds  23869  prdsxmslem2  24030  zcld  24321  xrge0tsms  24342  metdsf  24356  metdsge  24357  minveclem1  24933  minveclem3b  24937  minveclem6  24943  uniioombllem4  25095  uniioombllem6  25097  ismbf3d  25163  i1f1lem  25198  reldv  25379  ellimc2  25386  limcflf  25390  limciun  25403  dvfval  25406  dvrec  25464  dvlipcn  25503  mdegle0  25587  ply1nzb  25632  quotlem  25805  taylfval  25863  ulmdvlem1  25904  ulmdvlem2  25905  ulmdvlem3  25906  psercn  25930  sqff1o  26676  lgsquadlem2  26874  disjxwwlksn  29148  disjxwwlkn  29157  numclwwlk3lem2  29627  grpoidval  29754  grpoidinv2  29756  grpoinv  29766  minvecolem1  30115  minvecolem5  30122  minvecolem6  30123  adjbdln  31324  dfcnv2  31889  intimafv  31920  rexdiv  32080  gsumpart  32195  xrge0tsmsd  32197  fedgmullem2  32704  irngval  32738  rspectopn  32836  zarcls  32843  zartopn  32844  esumnul  33035  esum0  33036  hasheuni  33072  esum2d  33080  ldgenpisyslem3  33152  measvuni  33201  measdivcstALTV  33212  ddemeas  33223  carsgclctunlem2  33307  eulerpartlemgs2  33368  probfinmeasbALTV  33417  0rrv  33439  signsplypnf  33550  signsply0  33551  hgt750lemb  33657  bnj226  33734  bnj98  33867  bnj517  33885  bnj893  33928  bnj1137  33995  subfacf  34155  subfacp1lem6  34165  cvmsss2  34254  cvmliftlem1  34265  bj-rabtr  35799  relowlssretop  36233  fin2so  36464  matunitlindflem1  36473  ptrest  36476  poimirlem23  36500  poimirlem24  36501  poimirlem27  36504  poimirlem30  36507  poimirlem32  36509  cnambfre  36525  upixp  36586  0totbnd  36630  prdsbnd  36650  prdstotbnd  36651  cntotbnd  36653  rrnequiv  36692  ac6s6  37029  cdlemefrs32fva  39260  cdlemkid5  39795  cdlemk56  39831  dihf11lem  40126  addinvcom  41301  0dioph  41502  vdioph  41503  rmxyelqirrOLD  41635  pw2f1ocnv  41762  pwinfi  42301  eliunov2  42416  fvmptiunrelexplb0d  42421  fvmptiunrelexplb1d  42423  iunrelexp0  42439  ntrrn  42859  dssmapntrcls  42865  mnurndlem1  43026  wessf1ornlem  43868  axccdom  43907  mpteq1dfOLD  43925  fnmptif  43957  fsumiunss  44278  limcdm0  44321  liminfval2  44471  liminflelimsuplem  44478  cnrefiisplem  44532  0cnf  44580  dvsinax  44616  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnprodlem3  44651  iblempty  44668  fourierdlem89  44898  fourierdlem91  44900  fourierdlem100  44909  fourierdlem108  44917  fourierdlem112  44921  salexct3  45045  salgensscntex  45047  omeiunle  45220  0ome  45232  hoissrrn  45252  ovn0  45269  hoissrrn2  45281  hspmbl  45332  ovolval5lem2  45356  iunhoiioolem  45378  vonioolem2  45384  vonicclem2  45387  smflimlem1  45474  smfsuplem1  45514  smfinflem  45520  smflimsuplem1  45523  smflimsuplem2  45524  smflimsuplem3  45525  smflimsuplem4  45526  smflimsuplem5  45527  smflimsuplem7  45529  smfliminflem  45533  ralndv2  45801  iccelpart  46088  eliunxp2  46963  1arymaptf1  47282