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 4264 | . 2 ⊢ ¬ 〈𝐴, 𝐵〉 ∈ ∅ | |
2 | df-br 5075 | . 2 ⊢ (𝐴∅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ∅) | |
3 | 1, 2 | mtbir 323 | 1 ⊢ ¬ 𝐴∅𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2106 ∅c0 4256 〈cop 4567 class class class wbr 5074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-dif 3890 df-nul 4257 df-br 5075 |
This theorem is referenced by: sbcbr123 5128 sbcbr 5129 cnv0 6044 co02 6164 fvmptopabOLD 7330 brfvopab 7332 0we1 8336 brdom3 10284 canthwe 10407 relexpindlem 14774 join0 18123 meet0 18124 acycgr0v 33110 prclisacycgr 33113 disjALTV0 36862 brnonrel 41197 upwlkbprop 45300 |
Copyright terms: Public domain | W3C validator |