Theorem sbsbc 3749

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 208  [wsb 2091  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746

This theorem is referenced by:  spsbc  3758  sbcid  3762  sbccow  3768  sbcco  3771  sbcco2  3772  sbcie2g  3785  eqsbc1  3791  sbcralt  3826  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbnfc2  4394  csbab  4395  csbie2df  4398  2nreu  4399  frpoins2fg  6332  tfindes  7844  tfinds2  7845  setinds2f  9706  frins2f  9712  iuninc  32761  suppss2f  32841  fmptdF  32859  disjdsct  32906  esumpfinvalf  34374  measiuns  34515  bnj580  35209  bnj985v  35249  bnj985  35250  xpab  36077  bj-df-sb  37123  bj-sbeq  37387  bj-sbel1  37391  bj-snsetex  37449  poimirlem25  38145  poimirlem26  38146  fdc1  38246  exlimddvfi  38622  frege52b  44466  frege58c  44498  pm13.194  44989  pm14.12  44998  sbiota1  45011  onfrALTlem1  45125  onfrALTlem1VD  45466  disjinfi  45771  ellimcabssub0  46194  2reu8i  47708  ich2exprop  48078  ichnreuop  48079  ichreuopeq  48080