![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dm0 | 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 | eq0 3328 | . 2 ⊢ (dom ∅ = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom ∅) | |
2 | noel 3314 | . . . 4 ⊢ ¬ 〈𝑥, 𝑦〉 ∈ ∅ | |
3 | 2 | nex 1444 | . . 3 ⊢ ¬ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅ |
4 | vex 2644 | . . . 4 ⊢ 𝑥 ∈ V | |
5 | 4 | eldm2 4675 | . . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ∅) |
6 | 3, 5 | mtbir 637 | . 2 ⊢ ¬ 𝑥 ∈ dom ∅ |
7 | 1, 6 | mpgbir 1397 | 1 ⊢ dom ∅ = ∅ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 = wceq 1299 ∃wex 1436 ∈ wcel 1448 ∅c0 3310 〈cop 3477 dom cdm 4477 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-dif 3023 df-un 3025 df-nul 3311 df-sn 3480 df-pr 3481 df-op 3483 df-br 3876 df-dm 4487 |
This theorem is referenced by: rn0 4731 sqxpeq0 4898 fn0 5178 f0dom0 5252 f1o00 5336 rdg0 6214 frec0g 6224 ennnfonelemj0 11706 ennnfonelem1 11712 ennnfonelemkh 11717 ennnfonelemhf1o 11718 |
Copyright terms: Public domain | W3C validator |