Theorem br0 5079

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111  ∅c0 4243  ⟨cop 4531   class class class wbr 5030

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-dif 3884  df-nul 4244  df-br 5031

This theorem is referenced by:  sbcbr123  5084  sbcbr  5085  cnv0  5966  co02  6080  fvmptopab  7188  brfvopab  7190  0we1  8114  brdom3  9939  canthwe  10062  relexpindlem  14414  meet0  17739  join0  17740  acycgr0v  32508  prclisacycgr  32511  disjALTV0  36144  brnonrel  40289  upwlkbprop  44366