Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbsbc Unicode version

Theorem sbsbc 2937
 Description: Show that df-sb 1740 and df-sbc 2934 are equivalent when the class term in df-sbc 2934 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1740 for proofs involving df-sbc 2934. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbsbc

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2154 . 2
2 dfsbcq2 2936 . 2
31, 2ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wb 104  wsb 1739  wsbc 2933 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-clab 2141  df-cleq 2147  df-clel 2150  df-sbc 2934 This theorem is referenced by:  spsbc  2944  sbcid  2948  sbcco  2954  sbcco2  2955  sbcie2g  2966  eqsbc3  2972  sbcralt  3009  sbcrext  3010  sbnfc2  3087  csbabg  3088  cbvralcsf  3089  cbvrexcsf  3090  cbvreucsf  3091  cbvrabcsf  3092  isarep1  5249  finexdc  6836  ssfirab  6867  zsupcllemstep  11805  bezoutlemmain  11854  bdsbc  13379
 Copyright terms: Public domain W3C validator