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

Theorem sbsbc 2884
Description: Show that df-sb 1719 and df-sbc 2881 are equivalent when the class term  A in df-sbc 2881 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1719 for proofs involving df-sbc 2881. (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 2115 . 2  |-  y  =  y
2 dfsbcq2 2883 . 2  |-  ( y  =  y  ->  ( [ y  /  x ] ph  <->  [. y  /  x ]. ph ) )
31, 2ax-mp 5 1  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   [wsb 1718   [.wsbc 2880
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-clab 2102  df-cleq 2108  df-clel 2111  df-sbc 2881
This theorem is referenced by:  spsbc  2891  sbcid  2895  sbcco  2901  sbcco2  2902  sbcie2g  2912  eqsbc3  2918  sbcralt  2955  sbcrext  2956  sbnfc2  3028  csbabg  3029  cbvralcsf  3030  cbvrexcsf  3031  cbvreucsf  3032  cbvrabcsf  3033  isarep1  5177  finexdc  6762  ssfirab  6788  zsupcllemstep  11545  bezoutlemmain  11593  bdsbc  12890
  Copyright terms: Public domain W3C validator