Theorem br0 5147

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113  ∅c0 4285  ⟨cop 4586   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-nul 4286  df-br 5099

This theorem is referenced by:  sbcbr123  5152  sbcbr  5153  cnv0  6097  cnv0OLD  6098  co02  6219  brfvopab  7415  0we1  8433  brdom3  10438  canthwe  10562  relexpindlem  14986  join0  18326  meet0  18327  acycgr0v  35342  prclisacycgr  35345  disjALTV0  39013  brnonrel  43830  upwlkbprop  48384