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

Theorem sbcimg 3369
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 3330 . 2  |-  ( y  =  A  ->  ( [ y  /  x ] ( ph  ->  ps )  <->  [. A  /  x ]. ( ph  ->  ps ) ) )
2 dfsbcq2 3330 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
3 dfsbcq2 3330 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ps  <->  [. A  /  x ]. ps ) )
42, 3imbi12d 320 . 2  |-  ( y  =  A  ->  (
( [ y  /  x ] ph  ->  [ y  /  x ] ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )
5 sbim 2137 . 2  |-  ( [ y  /  x ]
( ph  ->  ps )  <->  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
)
61, 4, 5vtoclbg 3168 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395   [wsb 1740    e. wcel 1819   [.wsbc 3327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328
This theorem is referenced by:  sbcim1  3376  sbceqal  3383  sbc19.21g  3398  sbcssg  3943  iota4an  5576  sbcfung  5617  riotass2  6284  tfinds2  6697  telgsums  17149  sbcimi  30717  sbcim2g  33452  sbcssOLD  33456  onfrALTlem5  33457  sbcim2gVD  33818  sbcssgVD  33826  onfrALTlem5VD  33828  bnj538OLD  33940  bnj110  34059  bnj92  34063  bnj539  34092  bnj540  34093  cdlemkid3N  36802  cdlemkid4  36803  cdlemk35s  36806  cdlemk39s  36808  cdlemk42  36810
  Copyright terms: Public domain W3C validator