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

Step	Hyp	Ref	Expression
1		eqid 2082	. 2 |- y = y
2		dfsbcq2 2819	. 2 |- ( y = y -> ( [ y / x ] ph <-> [. y / x ]. ph ) )
3	1, 2	ax-mp 7	1 |- ( [ y / x ] ph <-> [. y / x ]. ph )

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