Theorem sbsbc 2844

Description: Show that df-sb 1693 and df-sbc 2841 are equivalent when the class term A in df-sbc 2841 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1693 for proofs involving df-sbc 2841. (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 2088	. 2 |- y = y
2		dfsbcq2 2843	. 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 103   [wsb 1692   [.wsbc 2840

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-clab 2075  df-cleq 2081  df-clel 2084  df-sbc 2841

This theorem is referenced by:  spsbc  2851  sbcid  2855  sbcco  2861  sbcco2  2862  sbcie2g  2872  eqsbc3  2878  sbcralt  2915  sbcrext  2916  sbnfc2  2988  csbabg  2989  cbvralcsf  2990  cbvrexcsf  2991  cbvreucsf  2992  cbvrabcsf  2993  isarep1  5100  finexdc  6618  ssfirab  6643  zsupcllemstep  11219  bezoutlemmain  11265  bdsbc  11749