Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dm0 | Structured version Visualization version GIF version |
Description: The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
dm0 | ⊢ dom ∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 4295 | . . . 4 ⊢ ¬ 〈𝑥, 𝑦〉 ∈ ∅ | |
2 | 1 | nex 1792 | . . 3 ⊢ ¬ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅ |
3 | vex 3498 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5764 | . . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅) |
5 | 2, 4 | mtbir 324 | . 2 ⊢ ¬ 𝑥 ∈ dom ∅ |
6 | 5 | nel0 4310 | 1 ⊢ dom ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∃wex 1771 ∈ wcel 2105 ∅c0 4290 〈cop 4565 dom cdm 5549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-dm 5559 |
This theorem is referenced by: rn0 5790 dmxpid 5794 dmxpss 6022 fn0 6473 f0dom0 6557 f10d 6642 f1o00 6643 0fv 6703 1stval 7682 bropopvvv 7776 bropfvvvv 7778 supp0 7826 tz7.44lem1 8032 tz7.44-2 8034 tz7.44-3 8035 oicl 8982 oif 8983 swrd0 14010 dmtrclfv 14368 symgsssg 18526 symgfisg 18527 psgnunilem5 18553 dvbsss 24429 perfdvf 24430 uhgr0e 26784 uhgr0 26786 usgr0 26953 egrsubgr 26987 0grsubgr 26988 vtxdg0e 27184 eupth0 27921 dmadjrnb 29611 eldmne0 30302 f1ocnt 30452 tocyccntz 30714 mbfmcst 31417 0rrv 31609 matunitlindf 34772 ismgmOLD 35011 conrel2d 39889 neicvgbex 40342 iblempty 42130 |
Copyright terms: Public domain | W3C validator |