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

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

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2457 . 2
2 dfsbcq2 3330 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  [wsb 1739  [.wsbc 3327
This theorem is referenced by:  spsbc  3340  sbcid  3344  sbcco  3350  sbcco2  3351  sbcie2g  3361  eqsbc3  3367  sbcralt  3408  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  sbnfc2  3854  csbab  3855  csbabgOLD  3856  isarep1  5672  tfindes  6697  tfinds2  6698  iuninc  27428  suppss2f  27477  fmptdF  27495  disjdsct  27521  esumpfinvalf  28082  measiuns  28188  setinds2f  29211  wfis2fg  29291  frins2fg  29327  fdc1  30239  exlimddvfi  30527  pm13.194  31319  pm14.12  31328  sbiota1  31341  ellimcabssub0  31623  onfrALTlem1  33320  onfrALTlem1VD  33690  bnj580  33971  bnj985  34011  bj-sbeq  34468  bj-sbel1  34472  bj-snsetex  34521  frege52b  37916  frege58c  37948  frege72  37963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328
  Copyright terms: Public domain W3C validator