| 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.) Avoid ax-10 2146, ax-11 2162, ax-12 2184. (Revised by TM, 24-Jan-2026.) |
| Ref | Expression |
|---|---|
| dm0rn0 | ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breq1 5101 | . . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑦)) | |
| 2 | breq2 5102 | . . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤)) | |
| 3 | 1, 2 | excomw 2047 | . . . . . . 7 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑦∃𝑧 𝑧𝐴𝑦) |
| 4 | breq2 5102 | . . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑥𝐴𝑦 ↔ 𝑥𝐴𝑤)) | |
| 5 | 1, 4 | sylan9bbr 510 | . . . . . . . 8 ⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑥) → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑤)) |
| 6 | 5 | cbvex2vw 2042 | . . . . . . 7 ⊢ (∃𝑦∃𝑧 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤) |
| 7 | 3, 6 | bitri 275 | . . . . . 6 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤) |
| 8 | 7 | notbii 320 | . . . . 5 ⊢ (¬ ∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤) |
| 9 | alnex 1782 | . . . . 5 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑧∃𝑦 𝑧𝐴𝑦) | |
| 10 | alnex 1782 | . . . . 5 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤) | |
| 11 | 8, 9, 10 | 3bitr4i 303 | . . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤) |
| 12 | noel 4290 | . . . . . 6 ⊢ ¬ 𝑧 ∈ ∅ | |
| 13 | 12 | nbn 372 | . . . . 5 ⊢ (¬ ∃𝑦 𝑧𝐴𝑦 ↔ (∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅)) |
| 14 | 13 | albii 1820 | . . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅)) |
| 15 | noel 4290 | . . . . . 6 ⊢ ¬ 𝑤 ∈ ∅ | |
| 16 | 15 | nbn 372 | . . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑤 ↔ (∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅)) |
| 17 | 16 | albii 1820 | . . . 4 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅)) |
| 18 | 11, 14, 17 | 3bitr3i 301 | . . 3 ⊢ (∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅) ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅)) |
| 19 | breq1 5101 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦)) | |
| 20 | 19 | exbidv 1922 | . . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦 𝑧𝐴𝑦)) |
| 21 | 20 | eqabcbw 2810 | . . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅)) |
| 22 | 4 | exbidv 1922 | . . . 4 ⊢ (𝑦 = 𝑤 → (∃𝑥 𝑥𝐴𝑦 ↔ ∃𝑥 𝑥𝐴𝑤)) |
| 23 | 22 | eqabcbw 2810 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅)) |
| 24 | 18, 21, 23 | 3bitr4i 303 | . 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
| 25 | df-dm 5634 | . . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
| 26 | 25 | eqeq1i 2741 | . 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅) |
| 27 | dfrn2 5837 | . . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | |
| 28 | 27 | eqeq1i 2741 | . 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) |
| 29 | 24, 26, 28 | 3bitr4i 303 | 1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1539 = wceq 1541 ∃wex 1780 ∈ wcel 2113 {cab 2714 ∅c0 4285 class class class wbr 5098 dom cdm 5624 ran crn 5625 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-cnv 5632 df-dm 5634 df-rn 5635 |
| This theorem is referenced by: rn0 5875 relrn0 5922 imadisj 6039 rnsnn0 6166 rnmpt0f 6201 f00 6716 f0rn0 6719 2nd0 7940 iinon 8272 onoviun 8275 onnseq 8276 map0b 8821 fodomfib 9229 fodomfibOLD 9231 intrnfi 9319 wdomtr 9480 noinfep 9569 wemapwe 9606 fin23lem31 10253 fin23lem40 10261 isf34lem7 10289 isf34lem6 10290 ttukeylem6 10424 fodomb 10436 rpnnen1lem4 12893 rpnnen1lem5 12894 fseqsupcl 13900 fseqsupubi 13901 dmtrclfv 14941 ruclem11 16165 prmreclem6 16849 0ram 16948 0ram2 16949 0ramcl 16951 gsumval2 18611 ghmrn 19158 gexex 19782 gsumval3 19836 subdrgint 20736 iinopn 22846 hauscmplem 23350 fbasrn 23828 alexsublem 23988 evth 24914 minveclem1 25380 minveclem3b 25384 ovollb2 25446 ovolunlem1a 25453 ovolunlem1 25454 ovoliunlem1 25459 ovoliun2 25463 ioombl1lem4 25518 uniioombllem1 25538 uniioombllem2 25540 uniioombllem6 25545 mbfsup 25621 mbfinf 25622 mbflimsup 25623 itg1climres 25671 itg2monolem1 25707 itg2mono 25710 itg2i1fseq2 25713 itg2cnlem1 25718 minvecolem1 30949 rge0scvg 34106 esumpcvgval 34235 cvmsss2 35468 fin2so 37808 ptrecube 37821 heicant 37856 isbnd3 37985 totbndbnd 37990 rnnonrel 43832 stoweidlem35 46279 hoicvr 46792 |
| Copyright terms: Public domain | W3C validator |