Theorem sbsbc 3036

Description: Show that df-sb 1811 and df-sbc 3033 are equivalent when the class term A in df-sbc 3033 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1811 for proofs involving df-sbc 3033. (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 2231	. 2 |- y = y
2		dfsbcq2 3035	. 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 1810   [.wsbc 3032

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-clab 2218  df-cleq 2224  df-clel 2227  df-sbc 3033

This theorem is referenced by:  spsbc  3044  sbcid  3048  sbcco  3054  sbcco2  3055  sbcie2g  3066  eqsbc1  3072  sbcralt  3109  sbcrext  3110  sbnfc2  3189  csbabg  3190  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  isarep1  5423  finexdc  7135  ssfirab  7172  zsupcllemstep  10552  bezoutlemmain  12649  bdsbc  16574