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

Theorem sbcimg 3265
Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
sbcimg

Proof of Theorem sbcimg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3227 . 2
2 dfsbcq2 3227 . . 3
3 dfsbcq2 3227 . . 3
42, 3imbi12d 313 . 2
5 sbim 2145 . 2
61, 4, 5vtoclbg 3071 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1670  [wsb 1676  e.wcel 1732  [.wsbc 3224
This theorem is referenced by:  sbcim1  3272  sbceqal  3279  sbcimdvOLD  3293  sbc19.21g  3296  sbcssg  3824  iota4an  5420  sbcfung  5461  riotass2  6090  tfinds2  6484  sbcim2g  30091  sbcssOLD  30095  onfrALTlem5  30096  sbcim2gVD  30457  sbcssgVD  30465  onfrALTlem5VD  30467  bnj538  30578  bnj110  30699  bnj92  30703  bnj539  30732  bnj540  30733  cdlemkid3N  33280  cdlemkid4  33281  cdlemk35s  33284  cdlemk39s  33286  cdlemk42  33288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-v 3017  df-sbc 3225
  Copyright terms: Public domain W3C validator