![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > rneq | Unicode version |
Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
Ref | Expression |
---|---|
rneq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveq 5005 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | dmeqd 5031 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-rn 4848 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-rn 4848 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2461 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: rneqi 5055 rneqd 5056 feq1 5535 foeq1 5608 fnrnfv 5732 fconst5 5908 frxp 6415 tz7.44-2 6624 tz7.44-3 6625 map0e 7010 ixpsnf1o 7061 ordtypecbv 7442 ordtypelem3 7445 dfac8alem 7866 dfac8a 7867 dfac5lem3 7962 dfac9 7972 dfac12lem1 7979 dfac12r 7982 ackbij2 8079 isfin3ds 8165 fin23lem17 8174 fin23lem29 8177 fin23lem30 8178 fin23lem32 8180 fin23lem34 8182 fin23lem35 8183 fin23lem39 8186 fin23lem41 8188 isf33lem 8202 isf34lem6 8216 dcomex 8283 axdc2lem 8284 zorn2lem1 8332 zorn2g 8339 ttukey2g 8352 gruurn 8629 rpnnen1 10561 pnrmopn 17361 isi1f 19519 itg1val 19528 mpfrcl 19892 iscusgra 21418 isuvtx 21450 ex-rn 21701 gidval 21754 grpoinvfval 21765 grpodivfval 21783 gxfval 21798 isablo 21824 elghomlem1 21902 iscom2 21953 isdivrngo 21972 vci 21980 isvclem 22009 isnvlem 22042 isphg 22271 pj11i 23166 hmopidmch 23609 hmopidmpj 23610 pjss1coi 23619 issibf 24601 sitgfval 24608 ghomgrplem 25053 elgiso 25060 relexprn 25089 dfrtrcl2 25101 rdgprc0 25364 rdgprc 25365 dfrdg2 25366 brrangeg 25689 axlowdimlem13 25797 axlowdim1 25802 volsupnfl 26150 dnnumch1 27009 aomclem3 27021 aomclem8 27027 isfrgra 28094 csbima12gALTVD 28718 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-rab 2675 df-v 2918 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-sn 3780 df-pr 3781 df-op 3783 df-br 4173 df-opab 4227 df-cnv 4845 df-dm 4847 df-rn 4848 |
Copyright terms: Public domain | W3C validator |