Theorem sbsbc 2968

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1762  [wsbc 2964

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2965

This theorem is referenced by:  spsbc  2976  sbcid  2980  sbcco  2986  sbcco2  2987  sbcie2g  2998  eqsbc1  3004  sbcralt  3041  sbcrext  3042  sbnfc2  3119  csbabg  3120  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  isarep1  5304  finexdc  6904  ssfirab  6935  zsupcllemstep  11948  bezoutlemmain  12001  bdsbc  14695