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

Theorem br0 5190
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 4326 . 2 ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
2 df-br 5142 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
31, 2mtbir 322 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2106  c0 4318  cop 4628   class class class wbr 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-dif 3947  df-nul 4319  df-br 5142
This theorem is referenced by:  sbcbr123  5195  sbcbr  5196  cnv0  6129  co02  6248  fvmptopabOLD  7448  brfvopab  7450  0we1  8488  brdom3  10505  canthwe  10628  relexpindlem  14992  join0  18340  meet0  18341  acycgr0v  33968  prclisacycgr  33971  disjALTV0  37427  brnonrel  42109  upwlkbprop  46286
  Copyright terms: Public domain W3C validator