![]() |
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 4326 | . 2 ⊢ ¬ 〈𝐴, 𝐵〉 ∈ ∅ | |
2 | df-br 5142 | . 2 ⊢ (𝐴∅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ∅) | |
3 | 1, 2 | mtbir 322 | 1 ⊢ ¬ 𝐴∅𝐵 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |