Theorem sbsbc 3754

Description: Show that df-sb 2066 and df-sbc 3751 are equivalent when the class term 𝐴 in df-sbc 3751 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2066 for proofs involving df-sbc 3751. (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 3753	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

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

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 3751

This theorem is referenced by:  spsbc  3763  sbcid  3767  sbccow  3773  sbcco  3776  sbcco2  3777  sbcie2g  3791  eqsbc1  3797  sbcralt  3832  cbvralcsf  3901  cbvreucsf  3903  cbvrabcsf  3904  sbnfc2  4398  csbab  4399  csbie2df  4402  2nreu  4403  frpoins2fg  6305  tfindes  7819  tfinds2  7820  frins2f  9682  iuninc  32539  suppss2f  32612  fmptdF  32630  disjdsct  32676  esumpfinvalf  34059  measiuns  34200  bnj580  34896  bnj985v  34936  bnj985  34937  xpab  35706  setinds2f  35760  bj-sbeq  36882  bj-sbel1  36886  bj-snsetex  36944  poimirlem25  37632  poimirlem26  37633  fdc1  37733  exlimddvfi  38109  frege52b  43871  frege58c  43903  pm13.194  44394  pm14.12  44403  sbiota1  44416  onfrALTlem1  44531  onfrALTlem1VD  44872  disjinfi  45179  ellimcabssub0  45608  2reu8i  47107  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467