Theorem sbsbc 2990

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1773  [wsbc 2986

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2987

This theorem is referenced by:  spsbc  2998  sbcid  3002  sbcco  3008  sbcco2  3009  sbcie2g  3020  eqsbc1  3026  sbcralt  3063  sbcrext  3064  sbnfc2  3142  csbabg  3143  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  isarep1  5341  finexdc  6960  ssfirab  6992  zsupcllemstep  12085  bezoutlemmain  12138  bdsbc  15420