Theorem sbsbc 2768

Description: Show that df-sb 1646 and df-sbc 2765 are equivalent when the class term A in df-sbc 2765 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1646 for proofs involving df-sbc 2765. (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 2040	. 2 |- y = y
2		dfsbcq2 2767	. 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 98   [wsb 1645   [.wsbc 2764

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-clab 2027  df-cleq 2033  df-clel 2036  df-sbc 2765

This theorem is referenced by:  spsbc  2775  sbcid  2779  sbcco  2785  sbcco2  2786  sbcie2g  2796  eqsbc3  2802  sbcralt  2834  sbcrext  2835  sbnfc2  2906  csbabg  2907  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  isarep1  4985  bdsbc  9978