MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcva Structured version   Unicode version

Theorem rspcva 3071
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcva  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcva
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 3069 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 429 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-v 2974
This theorem is referenced by:  rexraleqim  3085  fvcofneq  5851  suppssov1OLD  6317  caofinvl  6347  tfisi  6469  suppfnss  6714  suppssov1  6721  tfrlem1  6835  boxriin  7305  boxcutc  7306  marypha1lem  7683  marypha1  7684  supmo  7702  wemaplem2  7761  unwdomg  7799  noinfepOLD  7866  isinffi  8162  dfac9  8305  sornom  8446  fin23lem11  8486  fin1a2lem13  8581  axdc3lem2  8620  winalim2  8863  grothac  8997  nqereu  9098  infmrcl  10309  nnsub  10360  zextle  10715  xrsupsslem  11269  xrinfmsslem  11270  supxrunb1  11282  supxrunb2  11283  injresinjlem  11638  faclbnd4lem4  12072  rexuz3  12836  cau3lem  12842  caubnd2  12845  o1co  13064  climcn1  13069  incexclem  13299  dvdsext  13584  cshwsidrepsw  14120  prdsbasprj  14410  mreintcl  14533  isacs2  14591  acsfiel  14592  isdrs2  15109  lublecllem  15158  joinle  15184  meetle  15198  acsdrsel  15337  isacs4lem  15338  isacs5lem  15339  acsdrscl  15340  acsficl  15341  mgmidmo  15418  mrcmndind  15494  gsumval2  15513  symgfix2  15921  odeq  16053  gexid  16080  mplind  17584  evlslem1  17601  psgndiflemB  18030  mvmumamul1  18365  mdetunilem1  18418  m2detleiblem3  18435  m2detleiblem4  18436  cmpsublem  19002  cmpsub  19003  hauscmplem  19009  cmpfii  19012  ptpjcn  19184  isufil2  19481  ufileu  19492  cfiluweak  19870  cuspcvg  19876  lpbl  20078  lmmbr  20769  caussi  20808  mdeglt  21536  deg1lt  21569  ply1divex  21608  plyco0  21660  dgrco  21742  emcllem7  22395  isppw2  22453  pntleme  22857  pntlemp  22859  nbcusgra  23371  uvtxnbgra  23401  wlkdvspthlem  23506  grpoidinvlem3  23693  grpoideu  23696  lnconi  25437  ishashinf  26085  tpr2rico  26342  ofcfeqd2  26543  0elsiga  26557  sigaclci  26575  dya2icoseg2  26693  derangsn  27058  wfr3g  27723  frr3g  27767  heicant  28426  mblfinlem2  28429  ftc1anc  28475  fdc  28641  bndss  28685  isdrngo2  28764  divrngidl  28828  maxidlmax  28843  ismrcd1  29034  nacsfg  29041  isnacs3  29046  nacsfix  29048  mzpcl1  29065  mzpcl2  29066  mzpcong  29315  dnnumch1  29397  fnwe2lem2  29404  aomclem1  29407  aomclem4  29410  aomclem6  29412  lnr2i  29472  hbtlem5  29484  hbt  29486  ccats1rev  30260  clwwlkf  30456  clwwisshclwwlem1  30469  clwlkf1clwwlklem  30522  nbhashnn0  30532  vdiscusgra  30537  rusgraprop4  30556  rusgranumwlkl1lem1  30558  rusgranumwlks  30574  frgraunss  30587  vdn0frgrav2  30616  vdgn0frgrav2  30617  vdn1frgrav2  30618  vdgn1frgrav2  30619  usgn0fidegnn0  30622  frgrancvvdeqlem4  30626  frgraregorufr  30646  extwwlkfablem1  30667  numclwwlk1  30691  ssnn0fi  30746  suppssfz  30786  gsummoncoe1  30843  ply1mulgsumlem2  30845  mp2pm2mplem4  30919  lindslinindsimp2lem5  30996  lindslinindsimp2  30997  snlindsntor  31005  cdleme0nex  33934  dihglblem2N  34939  hgmapvs  35539
  Copyright terms: Public domain W3C validator