Theorem sbsbc 3781

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

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

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 3778

This theorem is referenced by:  spsbc  3790  sbcid  3794  sbccow  3800  sbcco  3803  sbcco2  3804  sbcie2g  3819  eqsbc1  3826  sbcralt  3866  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  sbnfc2  4436  csbab  4437  csbie2df  4440  2nreu  4441  frpoins2fg  6343  wfis2fgOLD  6356  isarep1OLD  6636  tfindes  7849  tfinds2  7850  frins2f  9745  iuninc  31780  suppss2f  31851  fmptdF  31869  disjdsct  31912  esumpfinvalf  33063  measiuns  33204  bnj580  33913  bnj985v  33953  bnj985  33954  xpab  34684  setinds2f  34740  bj-sbeq  35770  bj-sbel1  35774  bj-snsetex  35833  poimirlem25  36502  poimirlem26  36503  fdc1  36603  exlimddvfi  36979  frege52b  42626  frege58c  42658  pm13.194  43157  pm14.12  43166  sbiota1  43179  onfrALTlem1  43295  onfrALTlem1VD  43637  disjinfi  43877  ellimcabssub0  44320  2reu8i  45808  ich2exprop  46126  ichnreuop  46127  ichreuopeq  46128