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

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

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2157 . 2 𝑦 = 𝑦
2 dfsbcq2 2940 . 2 (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  [wsb 1742  [wsbc 2937
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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938
This theorem is referenced by:  spsbc  2948  sbcid  2952  sbcco  2958  sbcco2  2959  sbcie2g  2970  eqsbc3  2976  sbcralt  3013  sbcrext  3014  sbnfc2  3091  csbabg  3092  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  isarep1  5256  finexdc  6847  ssfirab  6878  zsupcllemstep  11832  bezoutlemmain  11882  bdsbc  13444
  Copyright terms: Public domain W3C validator