Theorem sbsbc 3742

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2098  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  spsbc  3751  sbcid  3755  sbccow  3761  sbcco  3764  sbcco2  3765  sbcie2g  3778  eqsbc1  3784  sbcralt  3818  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbnfc2  4396  csbab  4397  csbie2df  4400  2nreu  4401  frpoins2fg  6347  tfindes  7874  tfinds2  7875  setinds2f  9751  frins2f  9757  iuninc  33155  suppss2f  33232  fmptdf2  33250  disjdsct  33296  esumpfinvalf  34708  measiuns  34850  bnj580  35543  bnj985v  35583  bnj985  35584  xpab  36491  bj-df-sb  37549  bj-sbeq  37813  bj-sbel1  37817  bj-snsetex  37876  poimirlem25  38564  poimirlem26  38565  fdc1  38681  exlimddvfi  39055  frege52b  44889  frege58c  44921  pm13.194  45396  pm14.12  45405  sbiota1  45418  onfrALTlem1  45531  onfrALTlem1VD  45872  disjinfi  46207  ellimcabssub0  46629  2reu8i  48183  ich2exprop  48553  ichnreuop  48554  ichreuopeq  48555