Theorem sbsbc 2978

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1772  [wsbc 2974

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-clab 2174  df-cleq 2180  df-clel 2183  df-sbc 2975

This theorem is referenced by:  spsbc  2986  sbcid  2990  sbcco  2996  sbcco2  2997  sbcie2g  3008  eqsbc1  3014  sbcralt  3051  sbcrext  3052  sbnfc2  3129  csbabg  3130  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  isarep1  5314  finexdc  6915  ssfirab  6946  zsupcllemstep  11959  bezoutlemmain  12012  bdsbc  14881