![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imass1 | Structured version Visualization version Unicode version |
Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004.) |
Ref | Expression |
---|---|
imass1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssres 5107 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | rnss 5040 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-ima 4824 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-ima 4824 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3sstr4g 3440 |
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 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rab 2745 df-v 3014 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-nul 3699 df-if 3849 df-sn 3936 df-pr 3938 df-op 3942 df-br 4374 df-opab 4433 df-cnv 4819 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 |
This theorem is referenced by: vdwnnlem1 14955 dprdres 17671 imasnopn 20715 imasncld 20716 imasncls 20717 utoptop 21259 restutop 21262 ustuqtop3 21268 utopreg 21277 metustbl 21591 imadifxp 28220 esum2d 28920 eulerpartlemmf 29213 brtrclfv2 36320 frege97d 36345 frege109d 36350 frege131d 36357 hess 36376 |
Copyright terms: Public domain | W3C validator |