Theorem br0 5121

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

Syntax hints:  ¬ wn 3   ∈ wcel 2119  ∅c0 4261  ⟨cop 4561   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-dif 3886  df-nul 4262  df-br 5073

This theorem is referenced by:  sbcbr123  5126  sbcbr  5127  cnv0  6090  cnv0OLD  6091  co02  6212  brfvopab  7413  0we1  8431  brdom3  10441  canthwe  10565  relexpindlem  15016  join0  18360  meet0  18361  acycgr0v  35376  prclisacycgr  35379  disjALTV0  39221  brnonrel  44033  upwlkbprop  48629