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

Theorem rspcva 3052
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 3050 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 420 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707
This theorem is referenced by:  tfisi  4841  suppssov1  6305  caofinvl  6334  boxriin  7107  boxcutc  7108  marypha1lem  7441  marypha1  7442  supmo  7460  wemaplem2  7519  unwdomg  7555  noinfepOLD  7618  isinffi  7884  dfac9  8021  sornom  8162  fin23lem11  8202  fin1a2lem13  8297  axdc3lem2  8336  winalim2  8576  grothac  8710  nqereu  8811  infmrcl  9992  nnsub  10043  zextle  10348  xrsupsslem  10890  xrinfmsslem  10891  supxrunb1  10903  supxrunb2  10904  injresinjlem  11204  faclbnd4lem4  11592  rexuz3  12157  cau3lem  12163  caubnd2  12166  o1co  12385  climcn1  12390  incexclem  12621  dvdsext  12905  prdsbasprj  13699  mreintcl  13825  isacs2  13883  acsfiel  13884  isdrs2  14401  lubid  14444  acsdrsel  14598  isacs4lem  14599  isacs5lem  14600  acsdrscl  14601  acsficl  14602  mgmidmo  14698  gsumval2  14788  odeq  15193  gexid  15220  mplind  16567  cmpsublem  17467  cmpsub  17468  hauscmplem  17474  cmpfii  17477  ptpjcn  17648  isufil2  17945  ufileu  17956  cfiluweak  18330  cuspcvg  18336  lpbl  18538  lmmbr  19216  caussi  19255  evlslem1  19941  mdeglt  19993  deg1lt  20025  ply1divex  20064  plyco0  20116  dgrco  20198  emcllem7  20845  isppw2  20903  pntleme  21307  pntlemp  21309  nbcusgra  21477  uvtxnbgra  21507  wlkdvspthlem  21612  grpoidinvlem3  21799  grpoideu  21802  lnconi  23541  ishashinf  24164  kerf1hrm  24267  tpr2rico  24315  ofcfeqd2  24489  0elsiga  24502  sigaclci  24520  dya2icoseg2  24633  derangsn  24861  wfr3g  25542  frr3g  25586  heicant  26253  mblfinlem2  26256  ftc1anc  26302  fdc  26463  bndss  26509  isdrngo2  26588  divrngidl  26652  maxidlmax  26667  ismrcd1  26766  nacsfg  26773  isnacs3  26778  nacsfix  26780  mzpcl1  26800  mzpcl2  26801  mzpcong  27051  dnnumch1  27133  fnwe2lem2  27140  aomclem1  27143  aomclem4  27146  aomclem6  27148  lnr2i  27311  hbtlem5  27323  hbt  27325  nbhashnn0  28430  vdiscusgra  28435  frgraunss  28459  vdn0frgrav2  28488  vdgn0frgrav2  28489  vdn1frgrav2  28490  vdgn1frgrav2  28491  frgrancvvdeqlem4  28496  frgraregorufr  28516  cdleme0nex  31161  dihglblem2N  32166  hgmapvs  32766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960
  Copyright terms: Public domain W3C validator