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

Theorem sbcimg 3211
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 3173 . 2
2 dfsbcq2 3173 . . 3
3 dfsbcq2 3173 . . 3
42, 3imbi12d 313 . 2
5 sbim 2140 . 2
61, 4, 5vtoclbg 3021 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1654  [wsb 1660  e.wcel 1728  [.wsbc 3170
This theorem is referenced by:  sbcim1  3218  sbceqal  3224  sbcimdvOLD  3238  sbc19.21g  3241  sbcssg  3764  tfinds2  4884  iota4an  5483  riotass2  6626  sbcfung  28142  sbcim2g  28862  sbcssOLD  28866  onfrALTlem5  28867  sbcim2gVD  29228  sbcssgVD  29236  onfrALTlem5VD  29238  bnj538  29349  bnj110  29470  bnj92  29474  bnj539  29503  bnj540  29504  cdlemkid3N  31970  cdlemkid4  31971  cdlemk35s  31974  cdlemk39s  31976  cdlemk42  31978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967  df-sbc 3171
  Copyright terms: Public domain W3C validator