Theorem sbsbc 2955

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 104  [wsb 1750  [wsbc 2951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-clab 2152  df-cleq 2158  df-clel 2161  df-sbc 2952

This theorem is referenced by:  spsbc  2962  sbcid  2966  sbcco  2972  sbcco2  2973  sbcie2g  2984  eqsbc1  2990  sbcralt  3027  sbcrext  3028  sbnfc2  3105  csbabg  3106  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  isarep1  5274  finexdc  6868  ssfirab  6899  zsupcllemstep  11878  bezoutlemmain  11931  bdsbc  13740