Theorem sbsbc 3748

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2096  [wsbc 3744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3745

This theorem is used by:  spsbc  3757  sbcid  3761  sbccow  3767  sbcco  3770  sbcco2  3771  sbcie2g  3784  eqsbc1  3790  sbcralt  3825  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbnfc2  4404  csbab  4405  csbie2df  4408  2nreu  4409  frpoins2fg  6345  tfindes  7855  tfinds2  7856  setinds2f  9715  frins2f  9721  iuninc  32914  suppss2f  32992  fmptdF  33010  disjdsct  33057  esumpfinvalf  34475  measiuns  34616  bnj580  35310  bnj985v  35350  bnj985  35351  xpab  36226  bj-df-sb  37300  bj-sbeq  37564  bj-sbel1  37568  bj-snsetex  37627  poimirlem25  38324  poimirlem26  38325  fdc1  38425  exlimddvfi  38799  frege52b  44643  frege58c  44675  pm13.194  45150  pm14.12  45159  sbiota1  45172  onfrALTlem1  45285  onfrALTlem1VD  45626  disjinfi  45938  ellimcabssub0  46361  2reu8i  47878  ich2exprop  48248  ichnreuop  48249  ichreuopeq  48250