Theorem br0 5162

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146  ∅c0 4286  ⟨cop 4597   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-nul 4287  df-br 5112

This theorem is used by:  sbcbr123  5167  sbcbr  5168  cnv0  5871  cnv0OLD  5872  co02  6264  brfvopab  7473  0we1  8493  brdom3  10523  canthwe  10647  relexpindlem  15120  join0  18477  meet0  18478  acycgr0v  35653  prclisacycgr  35656  disjALTV0  39536  brnonrel  44348  upwlkbprop  48936