Theorem sbsbc 3746

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2101  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743

This theorem is used by:  spsbc  3755  sbcid  3759  sbccow  3765  sbcco  3768  sbcco2  3769  sbcie2g  3782  eqsbc1  3788  sbcralt  3823  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbnfc2  4400  csbab  4401  csbie2df  4404  2nreu  4405  frpoins2fg  6362  tfindes  7895  tfinds2  7896  setinds2f  9775  frins2f  9781  iuninc  33224  suppss2f  33301  fmptdf2  33319  disjdsct  33364  esumpfinvalf  34775  measiuns  34917  bnj580  35610  bnj985v  35650  bnj985  35651  xpab  36668  bj-df-sb  37726  bj-sbeq  37990  bj-sbel1  37994  bj-snsetex  38053  poimirlem25  38754  poimirlem26  38755  fdc1  38871  exlimddvfi  39245  frege52b  45079  frege58c  45111  pm13.194  45586  pm14.12  45594  sbiota1  45607  onfrALTlem1  45720  onfrALTlem1VD  46061  disjinfi  46410  ellimcabssub0  46832  2reu8i  48387  ich2exprop  48756  ichnreuop  48757  ichreuopeq  48758