Theorem sbsbc 3724

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 209  [wsb 2069  [wsbc 3720

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721

This theorem is referenced by:  spsbc  3733  sbcid  3737  sbccow  3743  sbcco  3746  sbcco2  3747  sbcie2g  3759  eqsbc3  3765  sbcralt  3801  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  sbnfc2  4344  csbab  4345  csbie2df  4348  2nreu  4349  wfis2fg  6153  isarep1  6412  tfindes  7557  tfinds2  7558  iuninc  30324  suppss2f  30398  fmptdF  30419  disjdsct  30462  esumpfinvalf  31445  measiuns  31586  bnj580  32295  bnj985v  32335  bnj985  32336  setinds2f  33137  frpoins2fg  33195  frins2fg  33202  bj-sbeq  34342  bj-sbel1  34346  bj-snsetex  34399  poimirlem25  35082  poimirlem26  35083  fdc1  35184  exlimddvfi  35560  frege52b  40590  frege58c  40622  pm13.194  41116  pm14.12  41125  sbiota1  41138  onfrALTlem1  41254  onfrALTlem1VD  41596  disjinfi  41820  ellimcabssub0  42259  2reu8i  43669  ich2exprop  43988  ichnreuop  43989  ichreuopeq  43990