Theorem sbsbc 3009

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1786  [wsbc 3005

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-clab 2194  df-cleq 2200  df-clel 2203  df-sbc 3006

This theorem is referenced by:  spsbc  3017  sbcid  3021  sbcco  3027  sbcco2  3028  sbcie2g  3039  eqsbc1  3045  sbcralt  3082  sbcrext  3083  sbnfc2  3162  csbabg  3163  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  isarep1  5379  finexdc  7025  ssfirab  7059  zsupcllemstep  10409  bezoutlemmain  12434  bdsbc  15993