|   | 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 1780 | . . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦) | |
| 2 | excom 2161 | . . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
| 3 | 1, 2 | xchbinx 334 | . . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) | 
| 4 | alnex 1780 | . . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦) | |
| 5 | 3, 4 | bitr4i 278 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦) | 
| 6 | noel 4337 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
| 7 | 6 | nbn 372 | . . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | 
| 8 | 7 | albii 1818 | . . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | 
| 9 | noel 4337 | . . . . . 6 ⊢ ¬ 𝑦 ∈ ∅ | |
| 10 | 9 | nbn 372 | . . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | 
| 11 | 10 | albii 1818 | . . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | 
| 12 | 5, 8, 11 | 3bitr3i 301 | . . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | 
| 13 | eqabcb 2882 | . . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅)) | |
| 14 | eqabcb 2882 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅)) | |
| 15 | 12, 13, 14 | 3bitr4i 303 | . 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) | 
| 16 | df-dm 5694 | . . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
| 17 | 16 | eqeq1i 2741 | . 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅) | 
| 18 | dfrn2 5898 | . . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | |
| 19 | 18 | eqeq1i 2741 | . 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅) | 
| 20 | 15, 17, 19 | 3bitr4i 303 | 1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1537 = wceq 1539 ∃wex 1778 ∈ wcel 2107 {cab 2713 ∅c0 4332 class class class wbr 5142 dom cdm 5684 ran crn 5685 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 df-opab 5205 df-cnv 5692 df-dm 5694 df-rn 5695 | 
| This theorem is referenced by: rn0 5935 relrn0 5982 imadisj 6097 rnsnn0 6227 rnmpt0f 6262 f00 6789 f0rn0 6792 2nd0 8022 iinon 8381 onoviun 8384 onnseq 8385 map0b 8924 fodomfib 9370 fodomfibOLD 9372 intrnfi 9457 wdomtr 9616 noinfep 9701 wemapwe 9738 fin23lem31 10384 fin23lem40 10392 isf34lem7 10420 isf34lem6 10421 ttukeylem6 10555 fodomb 10567 rpnnen1lem4 13023 rpnnen1lem5 13024 fseqsupcl 14019 fseqsupubi 14020 dmtrclfv 15058 ruclem11 16277 prmreclem6 16960 0ram 17059 0ram2 17060 0ramcl 17062 gsumval2 18700 ghmrn 19248 gexex 19872 gsumval3 19926 subdrgint 20805 iinopn 22909 hauscmplem 23415 fbasrn 23893 alexsublem 24053 evth 24992 minveclem1 25459 minveclem3b 25463 ovollb2 25525 ovolunlem1a 25532 ovolunlem1 25533 ovoliunlem1 25538 ovoliun2 25542 ioombl1lem4 25597 uniioombllem1 25617 uniioombllem2 25619 uniioombllem6 25624 mbfsup 25700 mbfinf 25701 mbflimsup 25702 itg1climres 25750 itg2monolem1 25786 itg2mono 25789 itg2i1fseq2 25792 itg2cnlem1 25797 minvecolem1 30894 rge0scvg 33949 esumpcvgval 34080 cvmsss2 35280 fin2so 37615 ptrecube 37628 heicant 37663 isbnd3 37792 totbndbnd 37797 rnnonrel 43609 stoweidlem35 46055 hoicvr 46568 | 
| Copyright terms: Public domain | W3C validator |