Theorem sbsbc 3732

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2068  [wsbc 3728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729

This theorem is referenced by:  spsbc  3741  sbcid  3745  sbccow  3751  sbcco  3754  sbcco2  3755  sbcie2g  3769  eqsbc1  3775  sbcralt  3810  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  sbnfc2  4379  csbab  4380  csbie2df  4383  2nreu  4384  frpoins2fg  6308  tfindes  7814  tfinds2  7815  setinds2f  9671  frins2f  9677  iuninc  32630  suppss2f  32711  fmptdF  32729  disjdsct  32776  esumpfinvalf  34220  measiuns  34361  bnj580  35055  bnj985v  35095  bnj985  35096  xpab  35908  bj-df-sb  36944  bj-sbeq  37208  bj-sbel1  37212  bj-snsetex  37270  poimirlem25  37966  poimirlem26  37967  fdc1  38067  exlimddvfi  38443  frege52b  44316  frege58c  44348  pm13.194  44839  pm14.12  44848  sbiota1  44861  onfrALTlem1  44975  onfrALTlem1VD  45316  disjinfi  45622  ellimcabssub0  46047  2reu8i  47561  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933