Theorem sbsbc 3001

Description: Show that df-sb 1785 and df-sbc 2998 are equivalent when the class term 𝐴 in df-sbc 2998 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1785 for proofs involving df-sbc 2998. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.)

Assertion

Ref	Expression
sbsbc	⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Proof of Theorem sbsbc

Step	Hyp	Ref	Expression
1		eqid 2204	. 2 ⊢ 𝑦 = 𝑦
2		dfsbcq2 3000	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Syntax hints:   ↔ wb 105  [wsb 1784  [wsbc 2997

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-clab 2191  df-cleq 2197  df-clel 2200  df-sbc 2998

This theorem is referenced by:  spsbc  3009  sbcid  3013  sbcco  3019  sbcco2  3020  sbcie2g  3031  eqsbc1  3037  sbcralt  3074  sbcrext  3075  sbnfc2  3153  csbabg  3154  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  isarep1  5359  finexdc  6998  ssfirab  7032  zsupcllemstep  10370  bezoutlemmain  12290  bdsbc  15756