![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dm0rn0 | Structured version Visualization version Unicode version |
Description: An empty domain implies an empty range. (Contributed by NM, 21-May-1998.) |
Ref | Expression |
---|---|
dm0rn0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alnex 1667 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | excom 1929 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | xchbinx 312 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | alnex 1667 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitr4i 256 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | noel 3737 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() | |
7 | 6 | nbn 349 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | albii 1693 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | noel 3737 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() | |
10 | 9 | nbn 349 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | albii 1693 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 5, 8, 11 | 3bitr3i 279 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | abeq1 2563 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | abeq1 2563 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 12, 13, 14 | 3bitr4i 281 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | df-dm 4847 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
17 | 16 | eqeq1i 2458 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | dfrn2 5026 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 18 | eqeq1i 2458 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 15, 17, 19 | 3bitr4i 281 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-br 4406 df-opab 4465 df-cnv 4845 df-dm 4847 df-rn 4848 |
This theorem is referenced by: rn0 5089 relrn0 5095 imadisj 5190 ndmimaOLD 5209 rnsnn0 5305 f00 5770 f0rn0 5773 2nd0 6805 iinon 7064 onoviun 7067 onnseq 7068 map0b 7515 fodomfib 7856 intrnfi 7935 wdomtr 8095 noinfep 8170 wemapwe 8207 fin23lem31 8778 fin23lem40 8786 isf34lem7 8814 isf34lem6 8815 ttukeylem6 8949 fodomb 8959 rpnnen1lem4 11300 rpnnen1lem5 11301 fseqsupcl 12197 fseqsupubi 12198 dmtrclfv 13094 ruclem11 14304 prmreclem6 14877 0ram 14990 0ram2 14991 0ramcl 14993 gsumval2 16535 ghmrn 16908 gexex 17503 gsumval3 17553 iinopn 19944 hauscmplem 20433 fbasrn 20911 alexsublem 21071 evth 21999 minveclem1 22378 minveclem3b 22382 minveclem3bOLD 22394 ovollb2 22454 ovolunlem1a 22461 ovolunlem1 22462 ovoliunlem1 22467 ovoliun2 22471 ioombl1lem4 22526 uniioombllem1 22550 uniioombllem2 22552 uniioombllem2OLD 22553 uniioombllem6 22558 mbfsup 22632 mbfinf 22633 mbfinfOLD 22634 mbflimsup 22635 mbflimsupOLD 22636 itg1climres 22684 itg2monolem1 22720 itg2mono 22723 itg2i1fseq2 22726 itg2cnlem1 22731 minvecolem1 26528 rge0scvg 28767 esumpcvgval 28911 cvmsss2 30009 fin2so 31944 ptrecube 31952 heicant 31987 isbnd3 32128 totbndbnd 32133 rnnonrel 36209 stoweidlem35 37906 hoicvr 38380 |
Copyright terms: Public domain | W3C validator |