![]() |
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 3952 | . . . 4 ⊢ ¬ 〈𝑥, 𝑦〉 ∈ ∅ | |
2 | 1 | nex 1771 | . . 3 ⊢ ¬ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅ |
3 | vex 3234 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5354 | . . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅) |
5 | 2, 4 | mtbir 312 | . 2 ⊢ ¬ 𝑥 ∈ dom ∅ |
6 | 5 | nel0 3965 | 1 ⊢ dom ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∃wex 1744 ∈ wcel 2030 ∅c0 3948 〈cop 4216 dom cdm 5143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-dm 5153 |
This theorem is referenced by: dmxpid 5377 rn0 5409 dmxpss 5600 fn0 6049 f0dom0 6127 f10d 6208 f1o00 6209 0fv 6265 1stval 7212 bropopvvv 7300 bropfvvvv 7302 supp0 7345 tz7.44lem1 7546 tz7.44-2 7548 tz7.44-3 7549 oicl 8475 oif 8476 swrd0 13480 dmtrclfv 13803 strlemor0OLD 16015 symgsssg 17933 symgfisg 17934 psgnunilem5 17960 dvbsss 23711 perfdvf 23712 uhgr0e 26011 uhgr0 26013 usgr0 26180 egrsubgr 26214 0grsubgr 26215 vtxdg0e 26426 eupth0 27192 dmadjrnb 28893 f1ocnt 29687 mbfmcst 30449 0rrv 30641 matunitlindf 33537 ismgmOLD 33779 conrel2d 38273 neicvgbex 38727 iblempty 40499 |
Copyright terms: Public domain | W3C validator |