Theorem sbsbc 3746

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2065  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3743

This theorem is referenced by:  spsbc  3755  sbcid  3759  sbccow  3765  sbcco  3768  sbcco2  3769  sbcie2g  3783  eqsbc1  3789  sbcralt  3824  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbnfc2  4390  csbab  4391  csbie2df  4394  2nreu  4395  frpoins2fg  6292  tfindes  7796  tfinds2  7797  frins2f  9649  iuninc  32504  suppss2f  32582  fmptdF  32600  disjdsct  32646  esumpfinvalf  34049  measiuns  34190  bnj580  34886  bnj985v  34926  bnj985  34927  xpab  35709  setinds2f  35763  bj-sbeq  36885  bj-sbel1  36889  bj-snsetex  36947  poimirlem25  37635  poimirlem26  37636  fdc1  37736  exlimddvfi  38112  frege52b  43872  frege58c  43904  pm13.194  44395  pm14.12  44404  sbiota1  44417  onfrALTlem1  44532  onfrALTlem1VD  44873  disjinfi  45180  ellimcabssub0  45608  2reu8i  47107  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467