Theorem sbsbc 3715

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 205  [wsb 2068  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  spsbc  3724  sbcid  3728  sbccow  3734  sbcco  3737  sbcco2  3738  sbcie2g  3753  eqsbc1  3760  sbcralt  3801  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  sbnfc2  4367  csbab  4368  csbie2df  4371  2nreu  4372  frpoins2fg  6232  wfis2fgOLD  6245  isarep1  6506  tfindes  7684  tfinds2  7685  frins2f  9442  iuninc  30801  suppss2f  30875  fmptdF  30895  disjdsct  30937  esumpfinvalf  31944  measiuns  32085  bnj580  32793  bnj985v  32833  bnj985  32834  xpab  33579  setinds2f  33661  bj-sbeq  35013  bj-sbel1  35017  bj-snsetex  35080  poimirlem25  35729  poimirlem26  35730  fdc1  35831  exlimddvfi  36207  frege52b  41386  frege58c  41418  pm13.194  41919  pm14.12  41928  sbiota1  41941  onfrALTlem1  42057  onfrALTlem1VD  42399  disjinfi  42620  ellimcabssub0  43048  2reu8i  44492  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813