Theorem br0 5215

Description: The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)

Assertion

Ref	Expression
br0	⊢ ¬ 𝐴∅𝐵

Proof of Theorem br0

Step	Hyp	Ref	Expression
1		noel 4360	. 2 ⊢ ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
2		df-br 5167	. 2 ⊢ (𝐴∅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
3	1, 2	mtbir 323	1 ⊢ ¬ 𝐴∅𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2108  ∅c0 4352  ⟨cop 4654   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-nul 4353  df-br 5167

This theorem is referenced by:  sbcbr123  5220  sbcbr  5221  cnv0  6172  co02  6291  fvmptopabOLD  7505  brfvopab  7507  0we1  8562  brdom3  10597  canthwe  10720  relexpindlem  15112  join0  18475  meet0  18476  acycgr0v  35116  prclisacycgr  35119  disjALTV0  38710  brnonrel  43551  upwlkbprop  47861