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

Theorem rspcdv 3055
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1  |-  ( ph  ->  A  e.  B )
rspcdv.2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rspcdv  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Distinct variable groups:    x, A    x, B    ph, x    ch, x
Allowed substitution hint:    ps( x)

Proof of Theorem rspcdv
StepHypRef Expression
1 rspcdv.1 . 2  |-  ( ph  ->  A  e.  B )
2 rspcdv.2 . . 3  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
32biimpd 199 . 2  |-  ( (
ph  /\  x  =  A )  ->  ( ps  ->  ch ) )
41, 3rspcimdv 3053 1  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   A.wral 2705
This theorem is referenced by:  ralxfrd  4737  zindd  10371  ismri2dad  13862  mreexd  13867  mreexexlemd  13869  catcocl  13910  catass  13911  moni  13962  subccocl  14042  funcco  14068  fullfo  14109  fthf1  14114  nati  14152  sizeusglecusglem1  21493  fargshiftfva  21626  eupatrl  21690  esumcvg  24476  orvcelel  24727  onint1  26199  ralbinrald  27953  ralxfrd2  28072  cshwsame  28277  usg2wlkeq  28304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958
  Copyright terms: Public domain W3C validator