Theorem sbsbc 3767

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2063  [wsbc 3763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clab 2713  df-cleq 2726  df-clel 2808  df-sbc 3764

This theorem is referenced by:  spsbc  3776  sbcid  3780  sbccow  3786  sbcco  3789  sbcco2  3790  sbcie2g  3804  eqsbc1  3810  sbcralt  3845  cbvralcsf  3914  cbvreucsf  3916  cbvrabcsf  3917  sbnfc2  4412  csbab  4413  csbie2df  4416  2nreu  4417  frpoins2fg  6330  wfis2fgOLD  6343  isarep1OLD  6623  tfindes  7852  tfinds2  7853  frins2f  9759  iuninc  32474  suppss2f  32549  fmptdF  32567  disjdsct  32613  esumpfinvalf  34015  measiuns  34156  bnj580  34865  bnj985v  34905  bnj985  34906  xpab  35664  setinds2f  35718  bj-sbeq  36840  bj-sbel1  36844  bj-snsetex  36902  poimirlem25  37590  poimirlem26  37591  fdc1  37691  exlimddvfi  38067  frege52b  43838  frege58c  43870  pm13.194  44362  pm14.12  44371  sbiota1  44384  onfrALTlem1  44499  onfrALTlem1VD  44841  disjinfi  45143  ellimcabssub0  45576  2reu8i  47070  ich2exprop  47403  ichnreuop  47404  ichreuopeq  47405