Theorem sbsbc 2993

Description: Show that df-sb 1777 and df-sbc 2990 are equivalent when the class term A in df-sbc 2990 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1777 for proofs involving df-sbc 2990. (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 2196	. 2 |- y = y
2		dfsbcq2 2992	. 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 105   [wsb 1776   [.wsbc 2989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-clab 2183  df-cleq 2189  df-clel 2192  df-sbc 2990

This theorem is referenced by:  spsbc  3001  sbcid  3005  sbcco  3011  sbcco2  3012  sbcie2g  3023  eqsbc1  3029  sbcralt  3066  sbcrext  3067  sbnfc2  3145  csbabg  3146  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  isarep1  5345  finexdc  6972  ssfirab  7006  zsupcllemstep  10336  bezoutlemmain  12190  bdsbc  15588