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

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

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2205 . 2 𝑦 = 𝑦
2 dfsbcq2 3001 . 2 (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
Colors of variables: wff set class
Syntax hints:  wb 105  [wsb 1785  [wsbc 2998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187
This theorem depends on definitions:  df-bi 117  df-clab 2192  df-cleq 2198  df-clel 2201  df-sbc 2999
This theorem is referenced by:  spsbc  3010  sbcid  3014  sbcco  3020  sbcco2  3021  sbcie2g  3032  eqsbc1  3038  sbcralt  3075  sbcrext  3076  sbnfc2  3154  csbabg  3155  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  isarep1  5360  finexdc  6999  ssfirab  7033  zsupcllemstep  10372  bezoutlemmain  12319  bdsbc  15794
  Copyright terms: Public domain W3C validator