Theorem sbsbc 3778

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 208  [wsb 2069  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clab 2802  df-cleq 2816  df-clel 2895  df-sbc 3775

This theorem is referenced by:  spsbc  3787  sbcid  3791  sbccow  3797  sbcco  3800  sbcco2  3801  sbcie2g  3813  eqsbc3  3819  eqsbc3OLD  3820  sbcralt  3857  cbvralcsf  3927  cbvreucsf  3929  cbvrabcsf  3930  sbnfc2  4390  csbab  4391  csbie2df  4394  2nreu  4395  wfis2fg  6187  isarep1  6444  tfindes  7579  tfinds2  7580  iuninc  30314  suppss2f  30386  fmptdF  30403  disjdsct  30440  esumpfinvalf  31337  measiuns  31478  bnj580  32187  bnj985v  32227  bnj985  32228  setinds2f  33026  frpoins2fg  33084  frins2fg  33091  bj-sbeq  34220  bj-sbel1  34224  bj-snsetex  34277  poimirlem25  34919  poimirlem26  34920  fdc1  35023  exlimddvfi  35402  frege52b  40242  frege58c  40274  pm13.194  40751  pm14.12  40760  sbiota1  40773  onfrALTlem1  40889  onfrALTlem1VD  41231  disjinfi  41461  ellimcabssub0  41905  2reu8i  43319  ich2exprop  43640  ichnreuop  43641  ichreuopeq  43642