![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dm0rn0 | Structured version Visualization version GIF version |
Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) |
Ref | Expression |
---|---|
dm0rn0 | ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alnex 1777 | . . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦) | |
2 | excom 2159 | . . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
3 | 1, 2 | xchbinx 334 | . . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) |
4 | alnex 1777 | . . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
5 | 3, 4 | bitr4i 278 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦) |
6 | noel 4343 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
7 | 6 | nbn 372 | . . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
8 | 7 | albii 1815 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
9 | noel 4343 | . . . . . 6 ⊢ ¬ 𝑦 ∈ ∅ | |
10 | 9 | nbn 372 | . . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
11 | 10 | albii 1815 | . . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
12 | 5, 8, 11 | 3bitr3i 301 | . . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
13 | eqabcb 2880 | . . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | |
14 | eqabcb 2880 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | |
15 | 12, 13, 14 | 3bitr4i 303 | . 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
16 | df-dm 5698 | . . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
17 | 16 | eqeq1i 2739 | . 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅) |
18 | dfrn2 5901 | . . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | |
19 | 18 | eqeq1i 2739 | . 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
20 | 15, 17, 19 | 3bitr4i 303 | 1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1534 = wceq 1536 ∃wex 1775 ∈ wcel 2105 {cab 2711 ∅c0 4338 class class class wbr 5147 dom cdm 5688 ran crn 5689 |
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-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
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-nf 1780 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-cnv 5696 df-dm 5698 df-rn 5699 |
This theorem is referenced by: rn0 5938 relrn0 5985 imadisj 6099 rnsnn0 6229 rnmpt0f 6264 f00 6790 f0rn0 6793 2nd0 8019 iinon 8378 onoviun 8381 onnseq 8382 map0b 8921 fodomfib 9366 fodomfibOLD 9368 intrnfi 9453 wdomtr 9612 noinfep 9697 wemapwe 9734 fin23lem31 10380 fin23lem40 10388 isf34lem7 10416 isf34lem6 10417 ttukeylem6 10551 fodomb 10563 rpnnen1lem4 13019 rpnnen1lem5 13020 fseqsupcl 14014 fseqsupubi 14015 dmtrclfv 15053 ruclem11 16272 prmreclem6 16954 0ram 17053 0ram2 17054 0ramcl 17056 gsumval2 18711 ghmrn 19259 gexex 19885 gsumval3 19939 subdrgint 20820 iinopn 22923 hauscmplem 23429 fbasrn 23907 alexsublem 24067 evth 25004 minveclem1 25471 minveclem3b 25475 ovollb2 25537 ovolunlem1a 25544 ovolunlem1 25545 ovoliunlem1 25550 ovoliun2 25554 ioombl1lem4 25609 uniioombllem1 25629 uniioombllem2 25631 uniioombllem6 25636 mbfsup 25712 mbfinf 25713 mbflimsup 25714 itg1climres 25763 itg2monolem1 25799 itg2mono 25802 itg2i1fseq2 25805 itg2cnlem1 25810 minvecolem1 30902 rge0scvg 33909 esumpcvgval 34058 cvmsss2 35258 fin2so 37593 ptrecube 37606 heicant 37641 isbnd3 37770 totbndbnd 37775 rnnonrel 43580 stoweidlem35 45990 hoicvr 46503 |
Copyright terms: Public domain | W3C validator |