![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ima0 | Structured version Visualization version Unicode version |
Description: Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.) |
Ref | Expression |
---|---|
ima0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ima 4866 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | res0 5128 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | rneqi 5080 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | rn0 5105 |
. 2
![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | 3eqtri 2488 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pr 4653 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4417 df-opab 4476 df-xp 4859 df-cnv 4861 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 |
This theorem is referenced by: csbima12 5204 relimasn 5210 elimasni 5214 inisegn0 5219 dffv3 5884 supp0cosupp0 6981 imacosupp 6982 ecexr 7394 domunfican 7870 fodomfi 7876 efgrelexlema 17448 dprdsn 17718 cnindis 20357 cnhaus 20419 cmpfi 20472 xkouni 20663 xkoccn 20683 mbfima 22637 ismbf2d 22646 limcnlp 22882 mdeg0 23068 pserulm 23426 0pth 25349 spthispth 25352 1pthonlem2 25369 eupath2 25757 disjpreima 28243 imadifxp 28261 dstrvprob 29353 opelco3 30469 funpartlem 30758 poimirlem1 31986 poimirlem2 31987 poimirlem3 31988 poimirlem4 31989 poimirlem5 31990 poimirlem6 31991 poimirlem7 31992 poimirlem10 31995 poimirlem11 31996 poimirlem12 31997 poimirlem13 31998 poimirlem16 32001 poimirlem17 32002 poimirlem19 32004 poimirlem20 32005 poimirlem22 32007 poimirlem23 32008 poimirlem24 32009 poimirlem25 32010 poimirlem28 32013 poimirlem29 32014 poimirlem31 32016 he0 36425 sPthisPth 39760 pthdlem2 39794 0pth-av 39841 1pthdlem2 39851 |
Copyright terms: Public domain | W3C validator |