Theorem sbsbc 3746

Description: Show that df-sb 2100 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 2100 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 2762	. 2 ⊢ 𝑦 = 𝑦
2		dfsbcq2 3745	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2099  [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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743

This theorem is used by:  spsbc  3755  sbcid  3759  sbccow  3765  sbcco  3768  sbcco2  3769  sbcie2g  3782  eqsbc1  3788  sbcralt  3822  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  sbnfc2  4400  csbab  4401  csbie2df  4404  2nreu  4405  frpoins2fg  6346  tfindes  7862  tfinds2  7863  setinds2f  9732  frins2f  9738  iuninc  33018  suppss2f  33096  fmptdf2  33114  disjdsct  33160  esumpfinvalf  34571  measiuns  34713  bnj580  35407  bnj985v  35447  bnj985  35448  xpab  36290  bj-df-sb  37365  bj-sbeq  37629  bj-sbel1  37633  bj-snsetex  37692  poimirlem25  38379  poimirlem26  38380  fdc1  38481  exlimddvfi  38855  frege52b  44714  frege58c  44746  pm13.194  45221  pm14.12  45230  sbiota1  45243  onfrALTlem1  45356  onfrALTlem1VD  45697  disjinfi  46009  ellimcabssub0  46432  2reu8i  47986  ich2exprop  48356  ichnreuop  48357  ichreuopeq  48358