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

Theorem sbcimg 3045
Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
sbcimg  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )

Proof of Theorem sbcimg
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3007 . 2  |-  ( y  =  A  ->  ( [ y  /  x ] ( ph  ->  ps )  <->  [. A  /  x ]. ( ph  ->  ps ) ) )
2 dfsbcq2 3007 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
3 dfsbcq2 3007 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ps  <->  [. A  /  x ]. ps ) )
42, 3imbi12d 311 . 2  |-  ( y  =  A  ->  (
( [ y  /  x ] ph  ->  [ y  /  x ] ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )
5 sbim 2018 . 2  |-  ( [ y  /  x ]
( ph  ->  ps )  <->  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
)
61, 4, 5vtoclbg 2857 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   [wsb 1638    e. wcel 1696   [.wsbc 3004
This theorem is referenced by:  sbceqal  3055  sbcimdv  3065  sbc19.21g  3068  sbcss  3577  tfinds2  4670  iota4an  5254  riotass2  6348  sbcfun  28090  sbcim2g  28601  sbcssOLD  28605  onfrALTlem5  28606  sbcim2gVD  28967  sbcssVD  28975  onfrALTlem5VD  28977  bnj538  29085  bnj110  29206  bnj92  29210  bnj539  29239  bnj540  29240  cdlemkid3N  31744  cdlemkid4  31745  cdlemk35s  31748  cdlemk39s  31750  cdlemk42  31752
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-v 2803  df-sbc 3005
  Copyright terms: Public domain W3C validator