Theorem br0 5153

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2144  ∅c0 4277  ⟨cop 4834   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 4046  df-nul 4278  df-br 5103

This theorem is used by:  sbcbr123  5159  sbcbr  5160  cnv0  5861  cnv0OLD  5862  co02  6264  brfvopab  7479  0we1  8519  brdom3  10612  canthwe  10741  relexpindlem  15223  join0  18584  meet0  18585  acycgr0v  35991  prclisacycgr  35994  disjALTV0  39893  brnonrel  44696  upwlkbprop  49343