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

Theorem sbsbc 2762
 Description: Show that df-sb 1643 and df-sbc 2759 are equivalent when the class term A in df-sbc 2759 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1643 for proofs involving df-sbc 2759. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbsbc ([y / x]φ[y / x]φ)

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2037 . 2 y = y
2 dfsbcq2 2761 . 2 (y = y → ([y / x]φ[y / x]φ))
31, 2ax-mp 7 1 ([y / x]φ[y / x]φ)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  [wsb 1642  [wsbc 2758 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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-clab 2024  df-cleq 2030  df-clel 2033  df-sbc 2759 This theorem is referenced by:  spsbc  2769  sbcid  2773  sbcco  2779  sbcco2  2780  sbcie2g  2790  eqsbc3  2796  sbcralt  2828  sbcrext  2829  sbnfc2  2900  csbabg  2901  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  isarep1  4928  bdsbc  9293
 Copyright terms: Public domain W3C validator