Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reldm0 | Structured version Visualization version GIF version |
Description: A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) |
Ref | Expression |
---|---|
reldm0 | ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rel0 5166 | . . 3 ⊢ Rel ∅ | |
2 | eqrel 5132 | . . 3 ⊢ ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅))) | |
3 | 1, 2 | mpan2 703 | . 2 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅))) |
4 | eq0 3888 | . . 3 ⊢ (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴) | |
5 | alnex 1697 | . . . . . 6 ⊢ (∀𝑦 ¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ¬ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) | |
6 | vex 3176 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
7 | 6 | eldm2 5244 | . . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
8 | 5, 7 | xchbinxr 324 | . . . . 5 ⊢ (∀𝑦 ¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴) |
9 | noel 3878 | . . . . . . 7 ⊢ ¬ 〈𝑥, 𝑦〉 ∈ ∅ | |
10 | 9 | nbn 361 | . . . . . 6 ⊢ (¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
11 | 10 | albii 1737 | . . . . 5 ⊢ (∀𝑦 ¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
12 | 8, 11 | bitr3i 265 | . . . 4 ⊢ (¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
13 | 12 | albii 1737 | . . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
14 | 4, 13 | bitr2i 264 | . 2 ⊢ (∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅) ↔ dom 𝐴 = ∅) |
15 | 3, 14 | syl6bb 275 | 1 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∅c0 3874 〈cop 4131 dom cdm 5038 Rel wrel 5043 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-xp 5044 df-rel 5045 df-dm 5048 |
This theorem is referenced by: relrn0 5304 coeq0 5561 fnresdisj 5915 fn0 5924 fresaunres2 5989 funopsn 6319 fsnunfv 6358 frxp 7174 domss2 8004 swrd0 13286 setsres 15729 pmtrsn 17762 gsumval3 18131 00lsp 18802 metn0 21975 wlkn0 26055 usgravd00 26446 eupath 26508 dfrdg2 30945 mbfresfi 32626 mapfzcons1 36298 diophrw 36340 eldioph2lem1 36341 eldioph2lem2 36342 sge0cl 39274 1wlkn0 40825 eulerpath 41409 |
Copyright terms: Public domain | W3C validator |