Theorem sbsbc 2913

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

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 2121

This theorem depends on definitions:  df-bi 116  df-clab 2126  df-cleq 2132  df-clel 2135  df-sbc 2910

This theorem is referenced by:  spsbc  2920  sbcid  2924  sbcco  2930  sbcco2  2931  sbcie2g  2942  eqsbc3  2948  sbcralt  2985  sbcrext  2986  sbnfc2  3060  csbabg  3061  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  isarep1  5209  finexdc  6796  ssfirab  6822  zsupcllemstep  11638  bezoutlemmain  11686  bdsbc  13056