Theorem br0 5117

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114  ∅c0 4293  ⟨cop 4575   class class class wbr 5068

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-dif 3941  df-nul 4294  df-br 5069

This theorem is referenced by:  sbcbr123  5122  sbcbr  5123  cnv0  6001  co02  6115  fvmptopab  7211  brfvopab  7213  0we1  8133  brdom3  9952  canthwe  10075  meet0  17749  join0  17750  acycgr0v  32397  prclisacycgr  32400  disjALTV0  35986  brnonrel  39956  upwlkbprop  44020