Theorem br0 5156

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 4301	. 2 ⊢ ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
2		df-br 5108	. 2 ⊢ (𝐴∅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
3	1, 2	mtbir 323	1 ⊢ ¬ 𝐴∅𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2109  ∅c0 4296  ⟨cop 4595   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3917  df-nul 4297  df-br 5108

This theorem is referenced by:  sbcbr123  5161  sbcbr  5162  cnv0  6113  co02  6233  fvmptopabOLD  7444  brfvopab  7446  0we1  8470  brdom3  10481  canthwe  10604  relexpindlem  15029  join0  18364  meet0  18365  acycgr0v  35135  prclisacycgr  35138  disjALTV0  38746  brnonrel  43578  upwlkbprop  48126