Theorem sbsbc 3782

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 205  [wsb 2068  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779

This theorem is referenced by:  spsbc  3791  sbcid  3795  sbccow  3801  sbcco  3804  sbcco2  3805  sbcie2g  3820  eqsbc1  3827  sbcralt  3867  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  sbnfc2  4437  csbab  4438  csbie2df  4441  2nreu  4442  frpoins2fg  6346  wfis2fgOLD  6359  isarep1OLD  6639  tfindes  7852  tfinds2  7853  frins2f  9748  iuninc  31792  suppss2f  31863  fmptdF  31881  disjdsct  31924  esumpfinvalf  33074  measiuns  33215  bnj580  33924  bnj985v  33964  bnj985  33965  xpab  34695  setinds2f  34751  bj-sbeq  35781  bj-sbel1  35785  bj-snsetex  35844  poimirlem25  36513  poimirlem26  36514  fdc1  36614  exlimddvfi  36990  frege52b  42640  frege58c  42672  pm13.194  43171  pm14.12  43180  sbiota1  43193  onfrALTlem1  43309  onfrALTlem1VD  43651  disjinfi  43891  ellimcabssub0  44333  2reu8i  45821  ich2exprop  46139  ichnreuop  46140  ichreuopeq  46141