Theorem br0 5134

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114  ∅c0 4273  ⟨cop 4573   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-nul 4274  df-br 5086

This theorem is referenced by:  sbcbr123  5139  sbcbr  5140  cnv0  6103  cnv0OLD  6104  co02  6225  brfvopab  7424  0we1  8441  brdom3  10450  canthwe  10574  relexpindlem  15025  join0  18369  meet0  18370  acycgr0v  35330  prclisacycgr  35333  disjALTV0  39175  brnonrel  44016  upwlkbprop  48614