Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > br0 | Structured version Visualization version GIF version |
Description: The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
Ref | Expression |
---|---|
br0 | ⊢ ¬ 𝐴∅𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 4217 | . 2 ⊢ ¬ 〈𝐴, 𝐵〉 ∈ ∅ | |
2 | df-br 5028 | . 2 ⊢ (𝐴∅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ∅) | |
3 | 1, 2 | mtbir 326 | 1 ⊢ ¬ 𝐴∅𝐵 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |