![]() |
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 1776 | . . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦) | |
2 | excom 2152 | . . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
3 | 1, 2 | xchbinx 333 | . . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) |
4 | alnex 1776 | . . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
5 | 3, 4 | bitr4i 277 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦) |
6 | noel 4333 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
7 | 6 | nbn 371 | . . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
8 | 7 | albii 1814 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
9 | noel 4333 | . . . . . 6 ⊢ ¬ 𝑦 ∈ ∅ | |
10 | 9 | nbn 371 | . . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
11 | 10 | albii 1814 | . . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
12 | 5, 8, 11 | 3bitr3i 300 | . . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
13 | eqabcb 2868 | . . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | |
14 | eqabcb 2868 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | |
15 | 12, 13, 14 | 3bitr4i 302 | . 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
16 | df-dm 5692 | . . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
17 | 16 | eqeq1i 2731 | . 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅) |
18 | dfrn2 5895 | . . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | |
19 | 18 | eqeq1i 2731 | . 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
20 | 15, 17, 19 | 3bitr4i 302 | 1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1532 = wceq 1534 ∃wex 1774 ∈ wcel 2099 {cab 2703 ∅c0 4325 class class class wbr 5153 dom cdm 5682 ran crn 5683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 df-opab 5216 df-cnv 5690 df-dm 5692 df-rn 5693 |
This theorem is referenced by: rn0 5932 relrn0 5976 imadisj 6089 rnsnn0 6219 rnmpt0f 6254 f00 6784 f0rn0 6787 2nd0 8010 iinon 8370 onoviun 8373 onnseq 8374 map0b 8912 fodomfib 9371 fodomfibOLD 9373 intrnfi 9459 wdomtr 9618 noinfep 9703 wemapwe 9740 fin23lem31 10386 fin23lem40 10394 isf34lem7 10422 isf34lem6 10423 ttukeylem6 10557 fodomb 10569 rpnnen1lem4 13016 rpnnen1lem5 13017 fseqsupcl 13997 fseqsupubi 13998 dmtrclfv 15023 ruclem11 16242 prmreclem6 16923 0ram 17022 0ram2 17023 0ramcl 17025 gsumval2 18679 ghmrn 19223 gexex 19851 gsumval3 19905 subdrgint 20782 iinopn 22895 hauscmplem 23401 fbasrn 23879 alexsublem 24039 evth 24976 minveclem1 25443 minveclem3b 25447 ovollb2 25509 ovolunlem1a 25516 ovolunlem1 25517 ovoliunlem1 25522 ovoliun2 25526 ioombl1lem4 25581 uniioombllem1 25601 uniioombllem2 25603 uniioombllem6 25608 mbfsup 25684 mbfinf 25685 mbflimsup 25686 itg1climres 25735 itg2monolem1 25771 itg2mono 25774 itg2i1fseq2 25777 itg2cnlem1 25782 minvecolem1 30807 rge0scvg 33764 esumpcvgval 33911 cvmsss2 35102 fin2so 37308 ptrecube 37321 heicant 37356 isbnd3 37485 totbndbnd 37490 rnnonrel 43258 stoweidlem35 45656 hoicvr 46169 |
Copyright terms: Public domain | W3C validator |