MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbsbc Structured version   Visualization version   GIF version

Theorem sbsbc 3426
Description: Show that df-sb 1878 and df-sbc 3423 are equivalent when the class term 𝐴 in df-sbc 3423 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1878 for proofs involving df-sbc 3423. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbsbc ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2621 . 2 𝑦 = 𝑦
2 dfsbcq2 3425 . 2 (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  [wsb 1877  [wsbc 3422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-clab 2608  df-cleq 2614  df-clel 2617  df-sbc 3423
This theorem is referenced by:  spsbc  3435  sbcid  3439  sbcco  3445  sbcco2  3446  sbcie2g  3456  eqsbc3  3462  sbcralt  3497  cbvralcsf  3551  cbvreucsf  3553  cbvrabcsf  3554  sbnfc2  3985  csbab  3986  wfis2fg  5686  isarep1  5945  tfindes  7024  tfinds2  7025  iuninc  29265  suppss2f  29322  fmptdF  29339  disjdsct  29364  esumpfinvalf  29961  measiuns  30103  bnj580  30744  bnj985  30784  setinds2f  31438  frins2fg  31498  bj-sbeq  32596  bj-sbel1  32600  bj-snsetex  32651  poimirlem25  33105  poimirlem26  33106  fdc1  33213  exlimddvfi  33598  frege52b  37704  frege58c  37736  pm13.194  38134  pm14.12  38143  sbiota1  38156  onfrALTlem1  38284  csbabgOLD  38572  onfrALTlem1VD  38648  disjinfi  38889  ellimcabssub0  39285
  Copyright terms: Public domain W3C validator