Theorem br0 5160

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

Syntax hints:  ¬ wn 3   ∈ wcel 2143  ∅c0 4286  ⟨cop 4595   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3908  df-nul 4287  df-br 5110

This theorem is referenced by:  sbcbr123  5165  sbcbr  5166  cnv0  5869  cnv0OLD  5870  co02  6262  brfvopab  7467  0we1  8487  brdom3  10507  canthwe  10631  relexpindlem  15096  join0  18454  meet0  18455  acycgr0v  35640  prclisacycgr  35643  disjALTV0  39503  brnonrel  44315  upwlkbprop  48903