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

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

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2752 . 2 𝑦 = 𝑦
2 dfsbcq2 3571 . 2 (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  [wsb 2038  [wsbc 3568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-clab 2739  df-cleq 2745  df-clel 2748  df-sbc 3569
This theorem is referenced by:  spsbc  3581  sbcid  3585  sbcco  3591  sbcco2  3592  sbcie2g  3602  eqsbc3  3608  sbcralt  3643  cbvralcsf  3698  cbvreucsf  3700  cbvrabcsf  3701  sbnfc2  4142  csbab  4143  wfis2fg  5870  isarep1  6130  tfindes  7219  tfinds2  7220  iuninc  29678  suppss2f  29740  fmptdF  29757  disjdsct  29781  esumpfinvalf  30439  measiuns  30581  bnj580  31282  bnj985  31322  setinds2f  31981  frins2fg  32045  bj-sbeq  33194  bj-sbel1  33198  bj-snsetex  33249  poimirlem25  33739  poimirlem26  33740  fdc1  33847  exlimddvfi  34232  frege52b  38677  frege58c  38709  pm13.194  39107  pm14.12  39116  sbiota1  39129  onfrALTlem1  39257  csbabgOLD  39544  onfrALTlem1VD  39617  disjinfi  39871  ellimcabssub0  40344
  Copyright terms: Public domain W3C validator