![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imaeq2i | Structured version Visualization version Unicode version |
Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
Ref | Expression |
---|---|
imaeq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imaeq2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaeq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | imaeq2 5141 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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-xp 4817 df-cnv 4819 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 |
This theorem is referenced by: cnvimarndm 5166 dmco 5321 imain 5640 fnimapr 5912 ssimaex 5913 intpreima 5994 resfunexg 6115 imauni 6136 isoini2 6215 frnsuppeq 6913 imacosupp 6942 uniqs 7409 fiint 7834 jech9.3 8271 infxpenlem 8430 hsmexlem4 8845 frnnn0supp 10912 hashkf 12510 ghmeqker 16919 gsumval3lem1 17549 gsumval3lem2 17550 islinds2 19381 lindsind2 19387 snclseqg 21140 retopbas 21791 ismbf3d 22621 i1fima 22647 i1fd 22650 itg1addlem5 22669 limciun 22860 plyeq0 23176 0pth 25311 2pthlem2 25337 constr3pthlem3 25396 htth 26582 fcoinver 28222 ffs2 28320 ffsrn 28321 sibfof 29178 eulerpartgbij 29210 eulerpartlemmf 29213 eulerpartlemgh 29216 eulerpart 29220 fiblem 29236 orrvcval4 29302 cvmsss2 30002 opelco3 30425 poimirlem3 31944 poimirlem30 31971 mbfposadd 31989 itg2addnclem2 31995 ftc1anclem5 32022 ftc1anclem6 32023 pwfi2f1o 35955 brtrclfv2 36320 binomcxp 36706 sPthisPth 39811 0pth-av 39892 1pthdlem2 39902 |
Copyright terms: Public domain | W3C validator |