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

Theorem sbcimg 3253
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 3215 . 2
2 dfsbcq2 3215 . . 3
3 dfsbcq2 3215 . . 3
42, 3imbi12d 313 . 2
5 sbim 2137 . 2
61, 4, 5vtoclbg 3062 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1662  [wsb 1668  e.wcel 1724  [.wsbc 3212
This theorem is referenced by:  sbcim1  3260  sbceqal  3267  sbcimdvOLD  3281  sbc19.21g  3284  sbcssg  3811  iota4an  5399  sbcfung  5440  riotass2  6054  tfinds2  6439  sbcim2g  29814  sbcssOLD  29818  onfrALTlem5  29819  sbcim2gVD  30180  sbcssgVD  30188  onfrALTlem5VD  30190  bnj538  30301  bnj110  30422  bnj92  30426  bnj539  30455  bnj540  30456  cdlemkid3N  33003  cdlemkid4  33004  cdlemk35s  33007  cdlemk39s  33009  cdlemk42  33011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-v 3008  df-sbc 3213
  Copyright terms: Public domain W3C validator