![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rneq | Structured version Visualization version Unicode version |
Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
Ref | Expression |
---|---|
rneq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveq 5026 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | dmeqd 5055 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-rn 4863 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-rn 4863 |
. 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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 df-opab 4475 df-cnv 4860 df-dm 4862 df-rn 4863 |
This theorem is referenced by: rneqi 5079 rneqd 5080 feq1 5731 foeq1 5811 fnrnfv 5933 fconst5 6145 frxp 6932 tz7.44-2 7150 tz7.44-3 7151 ixpsnf1o 7587 ordtypecbv 8057 ordtypelem3 8060 dfac8alem 8485 dfac8a 8486 dfac5lem3 8581 dfac9 8591 dfac12lem1 8598 dfac12r 8601 ackbij2 8698 isfin3ds 8784 fin23lem17 8793 fin23lem29 8796 fin23lem30 8797 fin23lem32 8799 fin23lem34 8801 fin23lem35 8802 fin23lem39 8805 fin23lem41 8807 isf33lem 8821 isf34lem6 8835 dcomex 8902 axdc2lem 8903 zorn2lem1 8951 zorn2g 8958 ttukey2g 8971 gruurn 9248 rpnnen1 11323 relexp0g 13133 relexpsucnnr 13136 dfrtrcl2 13173 mpfrcl 18789 ply1frcl 18955 pnrmopn 20407 isi1f 22680 itg1val 22689 axlowdimlem13 25032 axlowdim1 25037 iscusgra 25232 isuvtx 25264 wwlk 25457 clwwlk 25542 rusgra0edg 25731 isfrgra 25766 ex-rn 25938 gidval 25989 grpoinvfval 26000 grpodivfval 26018 gxfval 26033 isablo 26059 elghomlem1OLD 26137 iscom2 26188 isdivrngo 26207 vci 26215 isvclem 26244 isnvlem 26277 isphg 26506 pj11i 27412 hmopidmch 27854 hmopidmpj 27855 pjss1coi 27864 padct 28355 locfinreflem 28715 locfinref 28716 issibf 29214 sitgfval 29222 mrsubvrs 30208 ghomgrplem 30355 elgiso 30362 rdgprc0 30488 rdgprc 30489 dfrdg2 30490 brrangeg 30751 poimirlem24 32008 volsupnfl 32029 dnnumch1 35946 aomclem3 35958 aomclem8 35963 rclexi 36266 rtrclex 36268 rtrclexi 36272 cnvrcl0 36276 dfrtrcl5 36280 dfrcl2 36310 csbima12gALTVD 37333 sge0val 38245 ausgrusgri 39302 0uhgrsubgr 39400 cusgrsize 39564 |
Copyright terms: Public domain | W3C validator |