Theorem sbsbc 3684

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

Syntax hints:   ↔ wb 209  [wsb 2074  [wsbc 3680

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-clab 2717  df-cleq 2730  df-clel 2811  df-sbc 3681

This theorem is referenced by:  spsbc  3693  sbcid  3697  sbccow  3703  sbcco  3706  sbcco2  3707  sbcie2g  3721  eqsbc3  3727  sbcralt  3763  cbvralcsf  3832  cbvreucsf  3834  cbvrabcsf  3835  sbnfc2  4326  csbab  4327  csbie2df  4330  2nreu  4331  wfis2fg  6166  isarep1  6427  tfindes  7598  tfinds2  7599  iuninc  30476  suppss2f  30550  fmptdF  30570  disjdsct  30612  esumpfinvalf  31616  measiuns  31757  bnj580  32466  bnj985v  32506  bnj985  32507  xpab  33252  setinds2f  33331  frpoins2fg  33389  frins2fg  33399  bj-sbeq  34732  bj-sbel1  34736  bj-snsetex  34798  poimirlem25  35447  poimirlem26  35448  fdc1  35549  exlimddvfi  35925  frege52b  41065  frege58c  41097  pm13.194  41590  pm14.12  41599  sbiota1  41612  onfrALTlem1  41728  onfrALTlem1VD  42070  disjinfi  42291  ellimcabssub0  42722  2reu8i  44167  ich2exprop  44486  ichnreuop  44487  ichreuopeq  44488