Theorem sbsbc 3808

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2064  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  spsbc  3817  sbcid  3821  sbccow  3827  sbcco  3830  sbcco2  3831  sbcie2g  3847  eqsbc1  3854  sbcralt  3894  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  sbnfc2  4462  csbab  4463  csbie2df  4466  2nreu  4467  frpoins2fg  6376  wfis2fgOLD  6389  isarep1OLD  6668  tfindes  7900  tfinds2  7901  frins2f  9822  iuninc  32583  suppss2f  32657  fmptdF  32674  disjdsct  32714  esumpfinvalf  34040  measiuns  34181  bnj580  34889  bnj985v  34929  bnj985  34930  xpab  35688  setinds2f  35743  bj-sbeq  36867  bj-sbel1  36871  bj-snsetex  36929  poimirlem25  37605  poimirlem26  37606  fdc1  37706  exlimddvfi  38082  frege52b  43851  frege58c  43883  pm13.194  44381  pm14.12  44390  sbiota1  44403  onfrALTlem1  44519  onfrALTlem1VD  44861  disjinfi  45099  ellimcabssub0  45538  2reu8i  47028  ich2exprop  47345  ichnreuop  47346  ichreuopeq  47347