Theorem sbsbc 3406

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 195  [wsb 1867  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403

This theorem is referenced by:  spsbc  3415  sbcid  3419  sbcco  3425  sbcco2  3426  sbcie2g  3436  eqsbc3  3442  sbcralt  3477  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbnfc2  3959  csbab  3960  wfis2fg  5634  isarep1  5891  tfindes  6954  tfinds2  6955  iuninc  28761  suppss2f  28819  fmptdF  28836  disjdsct  28863  esumpfinvalf  29465  measiuns  29607  bnj580  30237  bnj985  30277  setinds2f  30928  frins2fg  30988  bj-sbeq  32088  bj-sbel1  32092  bj-snsetex  32144  poimirlem25  32604  poimirlem26  32605  fdc1  32712  exlimddvfi  33097  frege52b  37203  frege58c  37235  pm13.194  37635  pm14.12  37644  sbiota1  37657  onfrALTlem1  37784  csbabgOLD  38072  onfrALTlem1VD  38148  disjinfi  38375  ellimcabssub0  38684