Theorem br0 5123

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106  ∅c0 4256  ⟨cop 4567   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-dif 3890  df-nul 4257  df-br 5075

This theorem is referenced by:  sbcbr123  5128  sbcbr  5129  cnv0  6044  co02  6164  fvmptopabOLD  7330  brfvopab  7332  0we1  8336  brdom3  10284  canthwe  10407  relexpindlem  14774  join0  18123  meet0  18124  acycgr0v  33110  prclisacycgr  33113  disjALTV0  36862  brnonrel  41197  upwlkbprop  45300