Theorem sbsbc 3746

Description: Show that df-sb 2069 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 2069 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 2737	. 2 ⊢ 𝑦 = 𝑦
2		dfsbcq2 3745	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clab 2716  df-cleq 2729  df-clel 2812  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  4393  csbab  4394  csbie2df  4397  2nreu  4398  frpoins2fg  6310  tfindes  7815  tfinds2  7816  setinds2f  9671  frins2f  9677  iuninc  32651  suppss2f  32732  fmptdF  32750  disjdsct  32797  esumpfinvalf  34258  measiuns  34399  bnj580  35093  bnj985v  35133  bnj985  35134  xpab  35946  bj-df-sb  36901  bj-sbeq  37153  bj-sbel1  37157  bj-snsetex  37215  poimirlem25  37900  poimirlem26  37901  fdc1  38001  exlimddvfi  38377  frege52b  44249  frege58c  44281  pm13.194  44772  pm14.12  44781  sbiota1  44794  onfrALTlem1  44908  onfrALTlem1VD  45249  disjinfi  45555  ellimcabssub0  45981  2reu8i  47477  ich2exprop  47835  ichnreuop  47836  ichreuopeq  47837