Theorem sbsbc 2989

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1773  [wsbc 2985

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2986

This theorem is referenced by:  spsbc  2997  sbcid  3001  sbcco  3007  sbcco2  3008  sbcie2g  3019  eqsbc1  3025  sbcralt  3062  sbcrext  3063  sbnfc2  3141  csbabg  3142  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  isarep1  5340  finexdc  6958  ssfirab  6990  zsupcllemstep  12082  bezoutlemmain  12135  bdsbc  15350