![]() |
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 5811 | . . 3 ⊢ Rel ∅ | |
2 | eqrel 5796 | . . 3 ⊢ ((Rel 𝐴 ∧ Rel ∅) → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅))) | |
3 | 1, 2 | mpan2 691 | . 2 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅))) |
4 | eq0 4355 | . . 3 ⊢ (dom 𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ dom 𝐴) | |
5 | alnex 1777 | . . . . . 6 ⊢ (∀𝑦 ¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ¬ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) | |
6 | vex 3481 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
7 | 6 | eldm2 5914 | . . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
8 | 5, 7 | xchbinxr 335 | . . . . 5 ⊢ (∀𝑦 ¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ¬ 𝑥 ∈ dom 𝐴) |
9 | noel 4343 | . . . . . . 7 ⊢ ¬ 〈𝑥, 𝑦〉 ∈ ∅ | |
10 | 9 | nbn 372 | . . . . . 6 ⊢ (¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
11 | 10 | albii 1815 | . . . . 5 ⊢ (∀𝑦 ¬ 〈𝑥, 𝑦〉 ∈ 𝐴 ↔ ∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
12 | 8, 11 | bitr3i 277 | . . . 4 ⊢ (¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
13 | 12 | albii 1815 | . . 3 ⊢ (∀𝑥 ¬ 𝑥 ∈ dom 𝐴 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅)) |
14 | 4, 13 | bitr2i 276 | . 2 ⊢ (∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ∅) ↔ dom 𝐴 = ∅) |
15 | 3, 14 | bitrdi 287 | 1 ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1534 = wceq 1536 ∃wex 1775 ∈ wcel 2105 ∅c0 4338 〈cop 4636 dom cdm 5688 Rel wrel 5693 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-xp 5694 df-rel 5695 df-dm 5698 |
This theorem is referenced by: relrn0 5985 relresdm1 6052 coeq0 6276 snres0 6319 fnresdisj 6688 fn0 6699 fresaunres2 6780 funopsn 7167 fsnunfv 7206 frxp 8149 frxp2 8167 frxp3 8174 domss2 9174 swrd0 14692 setsres 17211 pmtrsn 19551 gsumval3 19939 00lsp 20996 metn0 24385 noetasuplem2 27793 noetainflem2 27797 wlkn0 29653 eulerpath 30269 dfrdg2 35776 mbfresfi 37652 mapfzcons1 42704 diophrw 42746 eldioph2lem1 42747 eldioph2lem2 42748 tfsconcatb0 43333 tfsconcat0i 43334 tfsconcat0b 43335 sge0cl 46336 |
Copyright terms: Public domain | W3C validator |