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

Theorem rspcva 3064
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 3062 . 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 1364    e. wcel 1757   A.wral 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2714  df-v 2968
This theorem is referenced by:  rexraleqim  3078  fvcofneq  5843  suppssov1OLD  6310  caofinvl  6340  tfisi  6462  suppfnss  6707  suppssov1  6714  tfrlem1  6825  boxriin  7297  boxcutc  7298  marypha1lem  7675  marypha1  7676  supmo  7694  wemaplem2  7753  unwdomg  7791  noinfepOLD  7858  isinffi  8154  dfac9  8297  sornom  8438  fin23lem11  8478  fin1a2lem13  8573  axdc3lem2  8612  winalim2  8855  grothac  8989  nqereu  9090  infmrcl  10301  nnsub  10352  zextle  10707  xrsupsslem  11261  xrinfmsslem  11262  supxrunb1  11274  supxrunb2  11275  injresinjlem  11626  faclbnd4lem4  12060  rexuz3  12824  cau3lem  12830  caubnd2  12833  o1co  13052  climcn1  13057  incexclem  13286  dvdsext  13571  cshwsidrepsw  14107  prdsbasprj  14397  mreintcl  14520  isacs2  14578  acsfiel  14579  isdrs2  15096  lublecllem  15145  joinle  15171  meetle  15185  acsdrsel  15324  isacs4lem  15325  isacs5lem  15326  acsdrscl  15327  acsficl  15328  mgmidmo  15405  mrcmndind  15480  gsumval2  15497  symgfix2  15905  odeq  16037  gexid  16064  mplind  17520  psgndiflemB  17876  mvmumamul1  18211  mdetunilem1  18264  m2detleiblem3  18281  m2detleiblem4  18282  cmpsublem  18848  cmpsub  18849  hauscmplem  18855  cmpfii  18858  ptpjcn  19030  isufil2  19327  ufileu  19338  cfiluweak  19716  cuspcvg  19722  lpbl  19924  lmmbr  20615  caussi  20654  evlslem1  21371  mdeglt  21425  deg1lt  21458  ply1divex  21497  plyco0  21549  dgrco  21631  emcllem7  22284  isppw2  22342  pntleme  22746  pntlemp  22748  nbcusgra  23198  uvtxnbgra  23228  wlkdvspthlem  23333  grpoidinvlem3  23520  grpoideu  23523  lnconi  25264  ishashinf  25912  kerf1hrm  26149  tpr2rico  26200  ofcfeqd2  26401  0elsiga  26415  sigaclci  26433  dya2icoseg2  26551  derangsn  26910  wfr3g  27574  frr3g  27618  heicant  28274  mblfinlem2  28277  ftc1anc  28323  fdc  28489  bndss  28533  isdrngo2  28612  divrngidl  28676  maxidlmax  28691  ismrcd1  28883  nacsfg  28890  isnacs3  28895  nacsfix  28897  mzpcl1  28914  mzpcl2  28915  mzpcong  29164  dnnumch1  29246  fnwe2lem2  29253  aomclem1  29256  aomclem4  29259  aomclem6  29261  lnr2i  29321  hbtlem5  29333  hbt  29335  ccats1rev  30110  clwwlkf  30306  clwwisshclwwlem1  30319  clwlkf1clwwlklem  30372  nbhashnn0  30382  vdiscusgra  30387  rusgraprop4  30406  rusgranumwlkl1lem1  30408  rusgranumwlks  30424  frgraunss  30437  vdn0frgrav2  30466  vdgn0frgrav2  30467  vdn1frgrav2  30468  vdgn1frgrav2  30469  usgn0fidegnn0  30472  frgrancvvdeqlem4  30476  frgraregorufr  30496  extwwlkfablem1  30517  numclwwlk1  30541  lindslinindsimp2lem5  30768  lindslinindsimp2  30769  snlindsntor  30777  cdleme0nex  33570  dihglblem2N  34575  hgmapvs  35175
  Copyright terms: Public domain W3C validator