Theorem sbsbc 2917

Description: Show that df-sb 1737 and df-sbc 2914 are equivalent when the class term A in df-sbc 2914 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1737 for proofs involving df-sbc 2914. (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 2140	. 2 |- y = y
2		dfsbcq2 2916	. 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 1736   [.wsbc 2913

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-clab 2127  df-cleq 2133  df-clel 2136  df-sbc 2914

This theorem is referenced by:  spsbc  2924  sbcid  2928  sbcco  2934  sbcco2  2935  sbcie2g  2946  eqsbc3  2952  sbcralt  2989  sbcrext  2990  sbnfc2  3065  csbabg  3066  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  isarep1  5217  finexdc  6804  ssfirab  6830  zsupcllemstep  11674  bezoutlemmain  11722  bdsbc  13227