Theorem br0 5197

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106  ∅c0 4339  ⟨cop 4637   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-dif 3966  df-nul 4340  df-br 5149

This theorem is referenced by:  sbcbr123  5202  sbcbr  5203  cnv0  6163  co02  6282  fvmptopabOLD  7488  brfvopab  7490  0we1  8543  brdom3  10566  canthwe  10689  relexpindlem  15099  join0  18463  meet0  18464  acycgr0v  35133  prclisacycgr  35136  disjALTV0  38736  brnonrel  43579  upwlkbprop  47982