Theorem sbsbc 2937

Description: Show that df-sb 1740 and df-sbc 2934 are equivalent when the class term A in df-sbc 2934 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1740 for proofs involving df-sbc 2934. (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 2154	. 2 |- y = y
2		dfsbcq2 2936	. 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 1739   [.wsbc 2933

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 1487  ax-17 1503  ax-ial 1511  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-clab 2141  df-cleq 2147  df-clel 2150  df-sbc 2934

This theorem is referenced by:  spsbc  2944  sbcid  2948  sbcco  2954  sbcco2  2955  sbcie2g  2966  eqsbc3  2972  sbcralt  3009  sbcrext  3010  sbnfc2  3087  csbabg  3088  cbvralcsf  3089  cbvrexcsf  3090  cbvreucsf  3091  cbvrabcsf  3092  isarep1  5249  finexdc  6836  ssfirab  6867  zsupcllemstep  11805  bezoutlemmain  11854  bdsbc  13379