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

Theorem br0 5076
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 4217 . 2 ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
2 df-br 5028 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
31, 2mtbir 326 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2113  c0 4209  cop 4519   class class class wbr 5027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-dif 3844  df-nul 4210  df-br 5028
This theorem is referenced by:  sbcbr123  5081  sbcbr  5082  cnv0  5967  co02  6087  fvmptopab  7217  brfvopab  7219  0we1  8155  brdom3  10021  canthwe  10144  relexpindlem  14505  meet0  17856  join0  17857  acycgr0v  32673  prclisacycgr  32676  disjALTV0  36474  brnonrel  40726  upwlkbprop  44818
  Copyright terms: Public domain W3C validator