Theorem br0 5161

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

Syntax hints:  ¬ wn 3   ∈ wcel 2149  ∅c0 4294  ⟨cop 4597   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-dif 3916  df-nul 4295  df-br 5111

This theorem is referenced by:  sbcbr123  5166  sbcbr  5167  cnv0  5867  cnv0OLD  5868  co02  6260  brfvopab  7465  0we1  8487  brdom3  10508  canthwe  10632  relexpindlem  15096  join0  18455  meet0  18456  acycgr0v  35535  prclisacycgr  35538  disjALTV0  39388  brnonrel  44202  upwlkbprop  48787