Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dm0rn0 | Structured version Visualization version GIF version |
Description: An empty domain implies an empty range. (Contributed by NM, 21-May-1998.) |
Ref | Expression |
---|---|
dm0rn0 | ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alnex 1697 | . . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦) | |
2 | excom 2029 | . . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
3 | 1, 2 | xchbinx 323 | . . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) |
4 | alnex 1697 | . . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
5 | 3, 4 | bitr4i 266 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦) |
6 | noel 3878 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
7 | 6 | nbn 361 | . . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
8 | 7 | albii 1737 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
9 | noel 3878 | . . . . . 6 ⊢ ¬ 𝑦 ∈ ∅ | |
10 | 9 | nbn 361 | . . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
11 | 10 | albii 1737 | . . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
12 | 5, 8, 11 | 3bitr3i 289 | . . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
13 | abeq1 2720 | . . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | |
14 | abeq1 2720 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | |
15 | 12, 13, 14 | 3bitr4i 291 | . 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
16 | df-dm 5048 | . . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
17 | 16 | eqeq1i 2615 | . 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅) |
18 | dfrn2 5233 | . . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | |
19 | 18 | eqeq1i 2615 | . 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
20 | 15, 17, 19 | 3bitr4i 291 | 1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ∅c0 3874 class class class wbr 4583 dom cdm 5038 ran crn 5039 |
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-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
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-eu 2462 df-mo 2463 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-cnv 5046 df-dm 5048 df-rn 5049 |
This theorem is referenced by: rn0 5298 relrn0 5304 imadisj 5403 rnsnn0 5519 f00 6000 f0rn0 6003 2nd0 7066 iinon 7324 onoviun 7327 onnseq 7328 map0b 7782 fodomfib 8125 intrnfi 8205 wdomtr 8363 noinfep 8440 wemapwe 8477 fin23lem31 9048 fin23lem40 9056 isf34lem7 9084 isf34lem6 9085 ttukeylem6 9219 fodomb 9229 rpnnen1lem4 11693 rpnnen1lem5 11694 rpnnen1lem4OLD 11699 rpnnen1lem5OLD 11700 fseqsupcl 12638 fseqsupubi 12639 dmtrclfv 13607 ruclem11 14808 prmreclem6 15463 0ram 15562 0ram2 15563 0ramcl 15565 gsumval2 17103 ghmrn 17496 gexex 18079 gsumval3 18131 iinopn 20532 hauscmplem 21019 fbasrn 21498 alexsublem 21658 evth 22566 minveclem1 23003 minveclem3b 23007 ovollb2 23064 ovolunlem1a 23071 ovolunlem1 23072 ovoliunlem1 23077 ovoliun2 23081 ioombl1lem4 23136 uniioombllem1 23155 uniioombllem2 23157 uniioombllem6 23162 mbfsup 23237 mbfinf 23238 mbflimsup 23239 itg1climres 23287 itg2monolem1 23323 itg2mono 23326 itg2i1fseq2 23329 itg2cnlem1 23334 minvecolem1 27114 rge0scvg 29323 esumpcvgval 29467 cvmsss2 30510 fin2so 32566 ptrecube 32579 heicant 32614 isbnd3 32753 totbndbnd 32758 rnnonrel 36916 rnmpt0 38407 stoweidlem35 38928 hoicvr 39438 |
Copyright terms: Public domain | W3C validator |