Theorem sbsbc 3033

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 105  [wsb 1808  [wsbc 3029

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3030

This theorem is referenced by:  spsbc  3041  sbcid  3045  sbcco  3051  sbcco2  3052  sbcie2g  3063  eqsbc1  3069  sbcralt  3106  sbcrext  3107  sbnfc2  3186  csbabg  3187  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  isarep1  5413  finexdc  7085  ssfirab  7121  zsupcllemstep  10479  bezoutlemmain  12559  bdsbc  16389