Theorem sbsbc 3727

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

Syntax hints:   ↔ wb 207  [wsb 2073  [wsbc 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clab 2718  df-cleq 2731  df-clel 2814  df-sbc 3724

This theorem is referenced by:  spsbc  3736  sbcid  3740  sbccow  3746  sbcco  3749  sbcco2  3750  sbcie2g  3763  eqsbc1  3769  sbcralt  3804  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  sbnfc2  4368  csbab  4369  csbie2df  4372  2nreu  4373  frpoins2fg  6296  tfindes  7804  tfinds2  7805  setinds2f  9663  frins2f  9669  iuninc  32650  suppss2f  32731  fmptdF  32749  disjdsct  32796  esumpfinvalf  34269  measiuns  34410  bnj580  35104  bnj985v  35144  bnj985  35145  xpab  35963  bj-df-sb  36999  bj-sbeq  37263  bj-sbel1  37267  bj-snsetex  37325  poimirlem25  38021  poimirlem26  38022  fdc1  38122  exlimddvfi  38498  frege52b  44342  frege58c  44374  pm13.194  44865  pm14.12  44874  sbiota1  44887  onfrALTlem1  45001  onfrALTlem1VD  45342  disjinfi  45647  ellimcabssub0  46070  2reu8i  47584  ich2exprop  47954  ichnreuop  47955  ichreuopeq  47956