Theorem sbsbc 3035

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1810  [wsbc 3031

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-clab 2218  df-cleq 2224  df-clel 2227  df-sbc 3032

This theorem is referenced by:  spsbc  3043  sbcid  3047  sbcco  3053  sbcco2  3054  sbcie2g  3065  eqsbc1  3071  sbcralt  3108  sbcrext  3109  sbnfc2  3188  csbabg  3189  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  isarep1  5416  finexdc  7091  ssfirab  7128  zsupcllemstep  10488  bezoutlemmain  12568  bdsbc  16453