Theorem br0 5135

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111  ∅c0 4278  ⟨cop 4577   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-dif 3900  df-nul 4279  df-br 5087

This theorem is referenced by:  sbcbr123  5140  sbcbr  5141  cnv0  6082  co02  6203  brfvopab  7398  0we1  8416  brdom3  10414  canthwe  10537  relexpindlem  14965  join0  18304  meet0  18305  acycgr0v  35184  prclisacycgr  35187  disjALTV0  38792  brnonrel  43622  upwlkbprop  48169