Theorem br0 5168

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108  ∅c0 4308  ⟨cop 4607   class class class wbr 5119

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-dif 3929  df-nul 4309  df-br 5120

This theorem is referenced by:  sbcbr123  5173  sbcbr  5174  cnv0  6129  co02  6249  fvmptopabOLD  7462  brfvopab  7464  0we1  8518  brdom3  10542  canthwe  10665  relexpindlem  15082  join0  18415  meet0  18416  acycgr0v  35170  prclisacycgr  35173  disjALTV0  38772  brnonrel  43613  upwlkbprop  48113