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

Theorem sbsbc 2768
 Description: Show that df-sb 1646 and df-sbc 2765 are equivalent when the class term 𝐴 in df-sbc 2765 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1646 for proofs involving df-sbc 2765. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbsbc ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2040 . 2 𝑦 = 𝑦
2 dfsbcq2 2767 . 2 (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
31, 2ax-mp 7 1 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  [wsb 1645  [wsbc 2764 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-clab 2027  df-cleq 2033  df-clel 2036  df-sbc 2765 This theorem is referenced by:  spsbc  2775  sbcid  2779  sbcco  2785  sbcco2  2786  sbcie2g  2796  eqsbc3  2802  sbcralt  2834  sbcrext  2835  sbnfc2  2906  csbabg  2907  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  isarep1  4985  bdsbc  9978
 Copyright terms: Public domain W3C validator