Theorem sbsbc 3002

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1785  [wsbc 2998

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-clab 2192  df-cleq 2198  df-clel 2201  df-sbc 2999

This theorem is referenced by:  spsbc  3010  sbcid  3014  sbcco  3020  sbcco2  3021  sbcie2g  3032  eqsbc1  3038  sbcralt  3075  sbcrext  3076  sbnfc2  3154  csbabg  3155  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  isarep1  5360  finexdc  6999  ssfirab  7033  zsupcllemstep  10372  bezoutlemmain  12319  bdsbc  15794