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

Theorem br0 5112
 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 4300 . 2 ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
2 df-br 5064 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
31, 2mtbir 324 1 ¬ 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∈ wcel 2107  ∅c0 4295  ⟨cop 4570   class class class wbr 5063 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-dif 3943  df-nul 4296  df-br 5064 This theorem is referenced by:  sbcbr123  5117  sbcbr  5118  cnv0  5998  co02  6112  fvmptopab  7203  brfvopab  7205  0we1  8127  brdom3  9944  canthwe  10067  meet0  17742  join0  17743  acycgr0v  32298  prclisacycgr  32301  disjALTV0  35870  brnonrel  39833  upwlkbprop  43864
 Copyright terms: Public domain W3C validator