Theorem sbsbc 2959

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 104  [wsb 1755  [wsbc 2955

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956

This theorem is referenced by:  spsbc  2966  sbcid  2970  sbcco  2976  sbcco2  2977  sbcie2g  2988  eqsbc1  2994  sbcralt  3031  sbcrext  3032  sbnfc2  3109  csbabg  3110  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  isarep1  5284  finexdc  6880  ssfirab  6911  zsupcllemstep  11900  bezoutlemmain  11953  bdsbc  13893