![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imaeq2 | Structured version Visualization version Unicode version |
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
imaeq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseq2 5078 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rneqd 5040 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-ima 4825 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-ima 4825 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2511 |
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 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-rab 2746 df-v 3015 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 df-br 4375 df-opab 4434 df-xp 4818 df-cnv 4820 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 |
This theorem is referenced by: imaeq2i 5144 imaeq2d 5146 relimasn 5169 funimaexg 5642 ssimaex 5914 ssimaexg 5915 isoselem 6218 isowe2 6227 f1opw2 6510 fnse 6901 supp0cosupp0 6942 tz7.49 7149 ecexr 7355 fopwdom 7667 sbthlem2 7670 sbth 7679 ssenen 7733 domunfican 7831 fodomfi 7837 f1opwfi 7865 fipreima 7867 marypha1lem 7934 ordtypelem2 8021 ordtypelem3 8022 ordtypelem9 8028 dfac12lem2 8561 dfac12r 8563 ackbij2lem2 8657 ackbij2lem3 8658 r1om 8661 enfin2i 8738 zorn2lem6 8918 zorn2lem7 8919 isacs5lem 16426 acsdrscl 16427 gicsubgen 16953 efgrelexlema 17410 tgcn 20279 subbascn 20281 iscnp4 20290 cnpnei 20291 cnima 20292 iscncl 20296 cncls 20301 cnconst2 20310 cnrest2 20313 cnprest 20316 cnindis 20319 cncmp 20418 cmpfi 20434 2ndcomap 20484 ptbasfi 20607 xkoopn 20615 xkoccn 20645 txcnp 20646 ptcnplem 20647 txcnmpt 20650 ptrescn 20665 xkoco1cn 20683 xkoco2cn 20684 xkococn 20686 xkoinjcn 20713 elqtop 20723 qtopomap 20744 qtopcmap 20745 ordthmeolem 20827 fbasrn 20910 elfm 20973 elfm2 20974 elfm3 20976 imaelfm 20977 rnelfmlem 20978 rnelfm 20979 fmfnfmlem2 20981 fmfnfmlem3 20982 fmfnfmlem4 20983 fmco 20987 flffbas 21021 lmflf 21031 fcfneii 21063 ptcmplem3 21080 ptcmplem5 21082 ptcmpg 21083 cnextcn 21093 symgtgp 21127 ghmcnp 21140 eltsms 21158 tsmsf1o 21170 fmucnd 21318 ucnextcn 21330 metcnp3 21566 mbfdm 22596 ismbf 22598 mbfima 22600 ismbfd 22608 mbfimaopnlem 22623 mbfimaopn2 22625 i1fd 22651 ellimc2 22844 limcflf 22848 xrlimcnp 23906 ubthlem1 26524 disjpreima 28204 imadifxp 28221 qtophaus 28670 rrhre 28832 mbfmcnvima 29085 imambfm 29090 eulerpartgbij 29211 erdszelem1 29920 erdsze 29931 erdsze2lem2 29933 cvmscbv 29987 cvmsi 29994 cvmsval 29995 cvmliftlem15 30027 opelco3 30426 brimageg 30700 fnimage 30702 imageval 30703 fvimage 30704 filnetlem4 31043 ptrest 31941 ismtyhmeolem 32138 ismtybndlem 32140 heibor1lem 32143 lmhmfgima 35944 brtrclfv2 36321 csbfv12gALTVD 37293 icccncfext 37807 sge0f1o 38283 |
Copyright terms: Public domain | W3C validator |