Theorem sbsbc 3744

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2067  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  spsbc  3753  sbcid  3757  sbccow  3763  sbcco  3766  sbcco2  3767  sbcie2g  3781  eqsbc1  3787  sbcralt  3822  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  sbnfc2  4391  csbab  4392  csbie2df  4395  2nreu  4396  frpoins2fg  6302  tfindes  7805  tfinds2  7806  setinds2f  9661  frins2f  9667  iuninc  32637  suppss2f  32718  fmptdF  32736  disjdsct  32784  esumpfinvalf  34235  measiuns  34376  bnj580  35071  bnj985v  35111  bnj985  35112  xpab  35922  bj-df-sb  36855  bj-sbeq  37104  bj-sbel1  37108  bj-snsetex  37166  poimirlem25  37848  poimirlem26  37849  fdc1  37949  exlimddvfi  38325  frege52b  44151  frege58c  44183  pm13.194  44674  pm14.12  44683  sbiota1  44696  onfrALTlem1  44810  onfrALTlem1VD  45151  disjinfi  45457  ellimcabssub0  45884  2reu8i  47380  ich2exprop  47738  ichnreuop  47739  ichreuopeq  47740