Theorem sbsbc 3655

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 198  [wsb 2011  [wsbc 3651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-clab 2763  df-cleq 2769  df-clel 2773  df-sbc 3652

This theorem is referenced by:  spsbc  3664  sbcid  3668  sbcco  3674  sbcco2  3675  sbcie2g  3685  eqsbc3  3691  eqsbc3OLD  3692  sbcralt  3727  cbvralcsf  3782  cbvreucsf  3784  cbvrabcsf  3785  sbnfc2  4232  csbab  4233  wfis2fg  5970  isarep1  6222  tfindes  7340  tfinds2  7341  iuninc  29941  suppss2f  30004  fmptdF  30021  disjdsct  30046  esumpfinvalf  30736  measiuns  30878  bnj580  31582  bnj985  31622  setinds2f  32272  frins2fg  32336  bj-sbeq  33467  bj-sbel1  33471  bj-snsetex  33523  poimirlem25  34044  poimirlem26  34045  fdc1  34150  exlimddvfi  34533  frege52b  39121  frege58c  39153  pm13.194  39550  pm14.12  39559  sbiota1  39572  onfrALTlem1  39690  onfrALTlem1VD  40041  disjinfi  40285  ellimcabssub0  40739  2reu8i  42136