Theorem sbsbc 3055

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1815  [wsbc 3051

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052

This theorem is referenced by:  spsbc  3063  sbcid  3067  sbcco  3073  sbcco2  3074  sbcie2g  3085  eqsbc1  3091  sbcralt  3128  sbcrext  3129  sbnfc2  3208  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  isarep1  5465  finexdc  7200  ssfirab  7237  zsupcllemstep  10643  bezoutlemmain  12756  bdsbc  16801