Theorem br0 5076

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113  ∅c0 4209  ⟨cop 4519   class class class wbr 5027

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-dif 3844  df-nul 4210  df-br 5028

This theorem is referenced by:  sbcbr123  5081  sbcbr  5082  cnv0  5967  co02  6087  fvmptopab  7217  brfvopab  7219  0we1  8155  brdom3  10021  canthwe  10144  relexpindlem  14505  meet0  17856  join0  17857  acycgr0v  32673  prclisacycgr  32676  disjALTV0  36474  brnonrel  40726  upwlkbprop  44818