Theorem sbsbc 2880

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 104  [wsb 1716  [wsbc 2876

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-clab 2100  df-cleq 2106  df-clel 2109  df-sbc 2877

This theorem is referenced by:  spsbc  2887  sbcid  2891  sbcco  2897  sbcco2  2898  sbcie2g  2908  eqsbc3  2914  sbcralt  2951  sbcrext  2952  sbnfc2  3024  csbabg  3025  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  cbvrabcsf  3029  isarep1  5165  finexdc  6747  ssfirab  6772  zsupcllemstep  11480  bezoutlemmain  11526  bdsbc  12739