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

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

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2606 . 2 𝑦 = 𝑦
2 dfsbcq2 3401 . 2 (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
31, 2ax-mp 5 1 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  [wsb 1866  [wsbc 3398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-clab 2593  df-cleq 2599  df-clel 2602  df-sbc 3399
This theorem is referenced by:  spsbc  3411  sbcid  3415  sbcco  3421  sbcco2  3422  sbcie2g  3432  eqsbc3  3438  sbcralt  3473  cbvralcsf  3527  cbvreucsf  3529  cbvrabcsf  3530  sbnfc2  3955  csbab  3956  wfis2fg  5617  isarep1  5874  tfindes  6928  tfinds2  6929  iuninc  28564  suppss2f  28622  fmptdF  28639  disjdsct  28666  esumpfinvalf  29268  measiuns  29410  bnj580  30040  bnj985  30080  setinds2f  30731  frins2fg  30791  bj-sbeq  31888  bj-sbel1  31892  bj-snsetex  31944  poimirlem25  32404  poimirlem26  32405  fdc1  32512  exlimddvfi  32897  frege52b  37003  frege58c  37035  pm13.194  37435  pm14.12  37444  sbiota1  37457  onfrALTlem1  37584  csbabgOLD  37872  onfrALTlem1VD  37948  disjinfi  38175  ellimcabssub0  38485
  Copyright terms: Public domain W3C validator