Theorem br0 5159

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109  ∅c0 4299  ⟨cop 4598   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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2709  df-cleq 2722  df-clel 2804  df-dif 3920  df-nul 4300  df-br 5111

This theorem is referenced by:  sbcbr123  5164  sbcbr  5165  cnv0  6116  co02  6236  fvmptopabOLD  7447  brfvopab  7449  0we1  8473  brdom3  10488  canthwe  10611  relexpindlem  15036  join0  18371  meet0  18372  acycgr0v  35142  prclisacycgr  35145  disjALTV0  38753  brnonrel  43585  upwlkbprop  48130