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

Theorem br0 5123
Description: The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
Assertion
Ref Expression
br0 ¬ 𝐴𝐵

Proof of Theorem br0
StepHypRef Expression
1 noel 4264 . 2 ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
2 df-br 5075 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
31, 2mtbir 323 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2106  c0 4256  cop 4567   class class class wbr 5074
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-dif 3890  df-nul 4257  df-br 5075
This theorem is referenced by:  sbcbr123  5128  sbcbr  5129  cnv0  6044  co02  6164  fvmptopabOLD  7330  brfvopab  7332  0we1  8336  brdom3  10284  canthwe  10407  relexpindlem  14774  join0  18123  meet0  18124  acycgr0v  33110  prclisacycgr  33113  disjALTV0  36862  brnonrel  41197  upwlkbprop  45300
  Copyright terms: Public domain W3C validator