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

Theorem sbsbc 2745
Description: Show that df-sb 1628 and df-sbc 2742 are equivalent when the class term A in df-sbc 2742 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1628 for proofs involving df-sbc 2742. (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 2022 . 2 y = y
2 dfsbcq2 2744 . 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 1627  [wsbc 2741
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-clab 2009  df-cleq 2015  df-clel 2018  df-sbc 2742
This theorem is referenced by:  spsbc  2752  sbcid  2756  sbcco  2762  sbcco2  2763  sbcie2g  2773  eqsbc3  2779  sbcralt  2811  sbcrext  2812  sbnfc2  2883  csbabg  2884  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  isarep1  4911  bdsbc  7232
  Copyright terms: Public domain W3C validator