Theorem sbsbc 3743

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

Assertion

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

Proof of Theorem sbsbc

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2099  [wsbc 3739

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3740

This theorem is used by:  spsbc  3752  sbcid  3756  sbccow  3762  sbcco  3765  sbcco2  3766  sbcie2g  3779  eqsbc1  3785  sbcralt  3819  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  sbnfc2  4397  csbab  4398  csbie2df  4401  2nreu  4402  frpoins2fg  6344  tfindes  7865  tfinds2  7866  setinds2f  9736  frins2f  9742  iuninc  33066  suppss2f  33143  fmptdf2  33161  disjdsct  33207  esumpfinvalf  34619  measiuns  34761  bnj580  35455  bnj985v  35495  bnj985  35496  xpab  36388  bj-df-sb  37447  bj-sbeq  37711  bj-sbel1  37715  bj-snsetex  37774  poimirlem25  38459  poimirlem26  38460  fdc1  38561  exlimddvfi  38935  frege52b  44794  frege58c  44826  pm13.194  45301  pm14.12  45310  sbiota1  45323  onfrALTlem1  45436  onfrALTlem1VD  45777  disjinfi  46089  ellimcabssub0  46512  2reu8i  48066  ich2exprop  48436  ichnreuop  48437  ichreuopeq  48438