Theorem sbsbc 2908

Description: Show that df-sb 1736 and df-sbc 2905 are equivalent when the class term A in df-sbc 2905 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1736 for proofs involving df-sbc 2905. (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 2137	. 2 |- y = y
2		dfsbcq2 2907	. 2 |- ( y = y -> ( [ y / x ] ph <-> [. y / x ]. ph ) )
3	1, 2	ax-mp 5	1 |- ( [ y / x ] ph <-> [. y / x ]. ph )

Syntax hints:   <-> wb 104   [wsb 1735   [.wsbc 2904

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-clab 2124  df-cleq 2130  df-clel 2133  df-sbc 2905

This theorem is referenced by:  spsbc  2915  sbcid  2919  sbcco  2925  sbcco2  2926  sbcie2g  2937  eqsbc3  2943  sbcralt  2980  sbcrext  2981  sbnfc2  3055  csbabg  3056  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  isarep1  5204  finexdc  6789  ssfirab  6815  zsupcllemstep  11627  bezoutlemmain  11675  bdsbc  13045