Theorem br0 5190

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106  ∅c0 4318  ⟨cop 4628   class class class wbr 5141

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-dif 3947  df-nul 4319  df-br 5142

This theorem is referenced by:  sbcbr123  5195  sbcbr  5196  cnv0  6129  co02  6248  fvmptopabOLD  7448  brfvopab  7450  0we1  8488  brdom3  10505  canthwe  10628  relexpindlem  14992  join0  18340  meet0  18341  acycgr0v  33968  prclisacycgr  33971  disjALTV0  37427  brnonrel  42109  upwlkbprop  46286