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

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

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2082 . 2  |-  y  =  y
2 dfsbcq2 2819 . 2  |-  ( y  =  y  ->  ( [ y  /  x ] ph  <->  [. y  /  x ]. ph ) )
31, 2ax-mp 7 1  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   [wsb 1686   [.wsbc 2816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-clab 2069  df-cleq 2075  df-clel 2078  df-sbc 2817
This theorem is referenced by:  spsbc  2827  sbcid  2831  sbcco  2837  sbcco2  2838  sbcie2g  2848  eqsbc3  2854  sbcralt  2891  sbcrext  2892  sbnfc2  2963  csbabg  2964  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  isarep1  5016  zsupcllemstep  10485  bezoutlemmain  10531  bdsbc  10807
  Copyright terms: Public domain W3C validator