Theorem sbsbc 3721

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

Assertion

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

Proof of Theorem sbsbc

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clab 2717  df-cleq 2731  df-clel 2817  df-sbc 3718

This theorem is referenced by:  spsbc  3730  sbcid  3734  sbccow  3740  sbcco  3743  sbcco2  3744  sbcie2g  3759  eqsbc1  3766  sbcralt  3806  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  sbnfc2  4371  csbab  4372  csbie2df  4375  2nreu  4376  frpoins2fg  6251  wfis2fgOLD  6264  isarep1OLD  6531  tfindes  7718  tfinds2  7719  frins2f  9520  iuninc  30909  suppss2f  30983  fmptdF  31002  disjdsct  31044  esumpfinvalf  32053  measiuns  32194  bnj580  32902  bnj985v  32942  bnj985  32943  xpab  33686  setinds2f  33764  bj-sbeq  35095  bj-sbel1  35099  bj-snsetex  35162  poimirlem25  35811  poimirlem26  35812  fdc1  35913  exlimddvfi  36289  frege52b  41504  frege58c  41536  pm13.194  42037  pm14.12  42046  sbiota1  42059  onfrALTlem1  42175  onfrALTlem1VD  42517  disjinfi  42738  ellimcabssub0  43165  2reu8i  44616  ich2exprop  44934  ichnreuop  44935  ichreuopeq  44936