![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > imaeq2 | Structured version Unicode version |
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
imaeq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseq2 5212 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rneqd 5174 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-ima 4960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-ima 4960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2520 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-rab 2807 df-v 3078 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-nul 3745 df-if 3899 df-sn 3985 df-pr 3987 df-op 3991 df-br 4400 df-opab 4458 df-xp 4953 df-cnv 4955 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 |
This theorem is referenced by: imaeq2i 5274 imaeq2d 5276 relimasn 5299 funimaexg 5602 ssimaex 5864 ssimaexg 5865 isoselem 6140 isowe2 6149 f1opw2 6422 fnse 6798 supp0cosupp0 6837 tz7.49 7009 ecexr 7215 fopwdom 7528 sbthlem2 7531 sbth 7540 ssenen 7594 domunfican 7694 fodomfi 7700 f1opwfi 7725 fipreima 7727 marypha1lem 7793 ordtypelem2 7843 ordtypelem3 7844 ordtypelem9 7850 dfac12lem2 8423 dfac12r 8425 ackbij2lem2 8519 ackbij2lem3 8520 r1om 8523 enfin2i 8600 zorn2lem6 8780 zorn2lem7 8781 isacs5lem 15457 acsdrscl 15458 gicsubgen 15924 efgrelexlema 16366 gsumval3OLD 16502 tgcn 18987 subbascn 18989 iscnp4 18998 cnpnei 18999 cnima 19000 iscncl 19004 cncls 19009 cnconst2 19018 cnrest2 19021 cnprest 19024 cnindis 19027 cncmp 19126 cmpfi 19142 2ndcomap 19193 ptbasfi 19285 xkoopn 19293 xkoccn 19323 txcnp 19324 ptcnplem 19325 txcnmpt 19328 ptrescn 19343 xkoco1cn 19361 xkoco2cn 19362 xkococn 19364 xkoinjcn 19391 elqtop 19401 qtopomap 19422 qtopcmap 19423 ordthmeolem 19505 fbasrn 19588 elfm 19651 elfm2 19652 elfm3 19654 imaelfm 19655 rnelfmlem 19656 rnelfm 19657 fmfnfmlem2 19659 fmfnfmlem3 19660 fmfnfmlem4 19661 fmco 19665 flffbas 19699 lmflf 19709 fcfneii 19741 ptcmplem3 19757 ptcmplem5 19759 ptcmpg 19760 cnextcn 19770 symgtgp 19803 ghmcnp 19816 eltsms 19834 tsmsf1o 19850 fmucnd 19998 ucnextcn 20010 metcnp3 20246 mbfdm 21238 ismbf 21240 mbfima 21242 ismbfd 21250 mbfimaopnlem 21265 mbfimaopn2 21267 i1fd 21291 ellimc2 21484 limcflf 21488 xrlimcnp 22494 ubthlem1 24422 disjpreima 26078 imadifxp 26089 rrhre 26591 mbfmcnvima 26815 imambfm 26820 eulerpartgbij 26898 erdszelem1 27222 erdsze 27233 erdsze2lem2 27235 cvmscbv 27290 cvmsi 27297 cvmsval 27298 cvmliftlem15 27330 opelco3 27732 brimageg 28101 fnimage 28103 imageval 28104 fvimage 28105 ptrest 28572 filnetlem4 28749 ismtyhmeolem 28850 ismtybndlem 28852 heibor1lem 28855 lmhmfgima 29584 csbfv12gALTVD 31952 |
Copyright terms: Public domain | W3C validator |