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

Theorem rspcdv 2900
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 198 . 2  |-  ( (
ph  /\  x  =  A )  ->  ( ps  ->  ch ) )
41, 3rspcimdv 2898 1  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralxfrd  4564  zindd  10129  ismri2dad  13555  mreexd  13560  mreexexlemd  13562  catcocl  13603  catass  13604  moni  13655  subccocl  13735  funcco  13761  fullfo  13802  fthf1  13807  nati  13845  esumcvg  23469  orvcelel  23685  onint1  24960  imonclem  25916  iepiclem  25926  ralbinrald  28080  fargshiftfva  28384  eupatrl  28385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator