![]() |
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 1854 | . . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦) | |
2 | excom 2198 | . . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
3 | 1, 2 | xchbinx 323 | . . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) |
4 | alnex 1854 | . . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
5 | 3, 4 | bitr4i 267 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦) |
6 | noel 4067 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
7 | 6 | nbn 361 | . . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
8 | 7 | albii 1895 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) |
9 | noel 4067 | . . . . . 6 ⊢ ¬ 𝑦 ∈ ∅ | |
10 | 9 | nbn 361 | . . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
11 | 10 | albii 1895 | . . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
12 | 5, 8, 11 | 3bitr3i 290 | . . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) |
13 | abeq1 2882 | . . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | |
14 | abeq1 2882 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | |
15 | 12, 13, 14 | 3bitr4i 292 | . 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
16 | df-dm 5259 | . . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
17 | 16 | eqeq1i 2776 | . 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅) |
18 | dfrn2 5449 | . . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | |
19 | 18 | eqeq1i 2776 | . 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
20 | 15, 17, 19 | 3bitr4i 292 | 1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∀wal 1629 = wceq 1631 ∃wex 1852 ∈ wcel 2145 {cab 2757 ∅c0 4063 class class class wbr 4786 dom cdm 5249 ran crn 5250 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pr 5034 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-br 4787 df-opab 4847 df-cnv 5257 df-dm 5259 df-rn 5260 |
This theorem is referenced by: rn0 5515 relrn0 5521 imadisj 5625 rnsnn0 5742 f00 6227 f0rn0 6230 2nd0 7322 iinon 7590 onoviun 7593 onnseq 7594 map0b 8049 fodomfib 8396 intrnfi 8478 wdomtr 8636 noinfep 8721 wemapwe 8758 fin23lem31 9367 fin23lem40 9375 isf34lem7 9403 isf34lem6 9404 ttukeylem6 9538 fodomb 9550 rpnnen1lem4 12020 rpnnen1lem5 12021 rpnnen1lem4OLD 12026 rpnnen1lem5OLD 12027 fseqsupcl 12984 fseqsupubi 12985 dmtrclfv 13967 ruclem11 15175 prmreclem6 15832 0ram 15931 0ram2 15932 0ramcl 15934 gsumval2 17488 ghmrn 17881 gexex 18463 gsumval3 18515 iinopn 20927 hauscmplem 21430 fbasrn 21908 alexsublem 22068 evth 22978 minveclem1 23414 minveclem3b 23418 ovollb2 23477 ovolunlem1a 23484 ovolunlem1 23485 ovoliunlem1 23490 ovoliun2 23494 ioombl1lem4 23549 uniioombllem1 23569 uniioombllem2 23571 uniioombllem6 23576 mbfsup 23651 mbfinf 23652 mbflimsup 23653 itg1climres 23701 itg2monolem1 23737 itg2mono 23740 itg2i1fseq2 23743 itg2cnlem1 23748 minvecolem1 28070 rge0scvg 30335 esumpcvgval 30480 cvmsss2 31594 fin2so 33729 ptrecube 33742 heicant 33777 isbnd3 33915 totbndbnd 33920 rnnonrel 38423 rnmpt0 39930 stoweidlem35 40769 hoicvr 41282 |
Copyright terms: Public domain | W3C validator |