Theorem sbsbc 2941

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 104  [wsb 1742  [wsbc 2937

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938

This theorem is referenced by:  spsbc  2948  sbcid  2952  sbcco  2958  sbcco2  2959  sbcie2g  2970  eqsbc3  2976  sbcralt  3013  sbcrext  3014  sbnfc2  3091  csbabg  3092  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  isarep1  5256  finexdc  6847  ssfirab  6878  zsupcllemstep  11832  bezoutlemmain  11882  bdsbc  13444