Theorem rgenw 3058

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

Syntax hints:   ∈ wcel 2100  ∀wral 3054

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

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

This theorem is referenced by:  rgen2w  3059  reuss  4329  reuun1  4330  rabnc  4398  riinrab  5097  0disj  5149  iinexg  5356  epse  5669  xpiindi  5846  eliunxp  5848  opeliunxp2  5849  elrnmpti  5970  cnviin  6302  fnmpti  6708  eqfnfv  7049  eufnfv  7251  mpoeq12  7504  porpss  7743  iunex  7990  abrexex2  7991  mpoex  8101  suppssov1  8220  suppssov2  8221  suppssfv  8225  opeliunxp2f  8233  onnseq  8382  ixpssmap  8969  boxcutc  8978  nneneq  9251  nneneqOLD  9263  finsschain  9410  dfom3  9697  cantnfdm  9714  rankuni2b  9903  rankval4  9917  alephf1  10135  dfac4  10172  dfacacn  10192  infmap2  10267  cfeq0  10306  fin23lem28  10390  axdc2lem  10498  axcclem  10507  ac6  10530  iundom  10592  konigthlem  10618  iunctb  10624  tskmid  10890  supaddc  12243  supadd  12244  supmul1  12245  supmullem2  12247  supmul  12248  uzf  12887  seqof  14090  hashbclem  14481  rlimclim1  15568  fsumcom2  15799  ackbijnn  15853  fprodcom2  16007  lcmf0  16656  phisum  16813  sumhash  16919  ramcl  17052  prdsvallem  17490  prdsval  17491  prdsbas  17493  prdshom  17503  imasplusg  17553  imasmulr  17554  imasvsca  17556  imasip  17557  imasaddfnlem  17564  imasvscafn  17573  isfunc  17904  wunfunc  17941  wunfuncOLD  17942  isnat  17991  natffn  17993  wunnat  18000  wunnatOLD  18001  fucsect  18018  setcepi  18131  grpinvfval  18994  odfval  19552  dfod2  19584  ghmcyg  19916  gsum2d2lem  19993  gsum2d2  19994  gsumcom2  19995  dmdprd  20020  dprdval  20025  dprdf11  20045  dprd2d2  20066  dpjeq  20081  pgpfac1lem2  20097  pgpfac1lem3  20099  pgpfac1lem4  20100  mptscmfsupp0  20925  00lsp  20980  ocv0  21695  ofco2  22467  tgidm  22997  pptbas  23025  tgrest  23177  iscnp2  23257  ist1-3  23367  discmp  23416  1stcfb  23463  lly1stc  23514  disllycmp  23516  dis1stc  23517  comppfsc  23550  txbas  23585  ptbasfi  23599  ptpjopn  23630  dfac14  23636  ptrescn  23657  xkoptsub  23672  fclsval  24026  ptcmplem2  24071  ptcmplem3  24072  cnextrel  24081  tsmsfbas  24146  ustuqtop  24265  prdsxmetlem  24388  ressprdsds  24391  prdsxmslem2  24552  zcld  24843  xrge0tsms  24864  metdsf  24878  metdsge  24879  minveclem1  25466  minveclem3b  25470  minveclem6  25476  uniioombllem4  25629  uniioombllem6  25631  ismbf3d  25697  i1f1lem  25732  reldv  25913  ellimc2  25920  limcflf  25924  limciun  25937  dvfval  25940  dvrec  26001  dvlipcn  26041  mdegle0  26127  ply1nzb  26173  quotlem  26351  taylfval  26409  ulmdvlem1  26452  ulmdvlem2  26453  ulmdvlem3  26454  psercn  26479  sqff1o  27233  lgsquadlem2  27433  disjxwwlksn  29861  disjxwwlkn  29870  numclwwlk3lem2  30340  grpoidval  30469  grpoidinv2  30471  grpoinv  30481  minvecolem1  30830  minvecolem5  30837  minvecolem6  30838  adjbdln  32039  dfcnv2  32619  intimafv  32647  rexdiv  32815  gsumpart  32952  xrge0tsmsd  32955  fedgmullem2  33556  irngval  33592  rspectopn  33720  zarcls  33727  zartopn  33728  esumnul  33919  esum0  33920  hasheuni  33956  esum2d  33964  ldgenpisyslem3  34036  measvuni  34085  measdivcstALTV  34096  ddemeas  34107  carsgclctunlem2  34191  eulerpartlemgs2  34252  probfinmeasbALTV  34301  0rrv  34323  signsplypnf  34434  signsply0  34435  hgt750lemb  34540  bnj226  34617  bnj98  34750  bnj517  34768  bnj893  34811  bnj1137  34878  subfacf  35050  subfacp1lem6  35060  cvmsss2  35149  cvmliftlem1  35160  bj-rabtr  36684  relowlssretop  37117  fin2so  37355  matunitlindflem1  37364  ptrest  37367  poimirlem23  37391  poimirlem24  37392  poimirlem27  37395  poimirlem30  37398  poimirlem32  37400  cnambfre  37416  upixp  37477  0totbnd  37521  prdsbnd  37541  prdstotbnd  37542  cntotbnd  37544  rrnequiv  37583  ac6s6  37920  cdlemefrs32fva  40146  cdlemkid5  40681  cdlemk56  40717  dihf11lem  41012  addinvcom  42176  0dioph  42506  vdioph  42507  rmxyelqirrOLD  42639  pw2f1ocnv  42766  pwinfi  43302  eliunov2  43417  fvmptiunrelexplb0d  43422  fvmptiunrelexplb1d  43424  iunrelexp0  43440  ntrrn  43860  dssmapntrcls  43866  mnurndlem1  44026  wessf1ornlem  44862  axccdom  44899  mpteq1dfOLD  44914  fnmptif  44945  fsumiunss  45266  limcdm0  45309  liminfval2  45459  liminflelimsuplem  45466  cnrefiisplem  45520  0cnf  45568  dvsinax  45604  ioodvbdlimc1lem2  45623  ioodvbdlimc2lem  45625  dvnprodlem3  45639  iblempty  45656  fourierdlem89  45886  fourierdlem91  45888  fourierdlem100  45897  fourierdlem108  45905  fourierdlem112  45909  salexct3  46033  salgensscntex  46035  omeiunle  46208  0ome  46220  hoissrrn  46240  ovn0  46257  hoissrrn2  46269  hspmbl  46320  ovolval5lem2  46344  iunhoiioolem  46366  vonioolem2  46372  vonicclem2  46375  smflimlem1  46462  smfsuplem1  46502  smfinflem  46508  smflimsuplem1  46511  smflimsuplem2  46512  smflimsuplem3  46513  smflimsuplem4  46514  smflimsuplem5  46515  smflimsuplem7  46517  smfliminflem  46521  ralndv2  46789  iccelpart  47075  eliunxp2  47793  1arymaptf1  48111