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 4296 | . . . 4 ⊢ ¬ 〈𝑥, 𝑦〉 ∈ ∅ | |
2 | 1 | nex 1801 | . . 3 ⊢ ¬ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅ |
3 | vex 3497 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | eldm2 5770 | . . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅) |
5 | 2, 4 | mtbir 325 | . 2 ⊢ ¬ 𝑥 ∈ dom ∅ |
6 | 5 | nel0 4311 | 1 ⊢ dom ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∃wex 1780 ∈ wcel 2114 ∅c0 4291 〈cop 4573 dom cdm 5555 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-br 5067 df-dm 5565 |
This theorem is referenced by: rn0 5796 dmxpid 5800 dmxpss 6028 fn0 6479 f0dom0 6563 f10d 6648 f1o00 6649 0fv 6709 1stval 7691 bropopvvv 7785 bropfvvvv 7787 supp0 7835 tz7.44lem1 8041 tz7.44-2 8043 tz7.44-3 8044 oicl 8993 oif 8994 swrd0 14020 dmtrclfv 14378 symgsssg 18595 symgfisg 18596 psgnunilem5 18622 dvbsss 24500 perfdvf 24501 uhgr0e 26856 uhgr0 26858 usgr0 27025 egrsubgr 27059 0grsubgr 27060 vtxdg0e 27256 eupth0 27993 dmadjrnb 29683 eldmne0 30373 f1ocnt 30525 tocyccntz 30786 mbfmcst 31517 0rrv 31709 matunitlindf 34905 ismgmOLD 35143 conrel2d 40058 neicvgbex 40511 iblempty 42299 |
Copyright terms: Public domain | W3C validator |