Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rneq | Structured version Visualization version GIF version |
Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
Ref | Expression |
---|---|
rneq | ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveq 5218 | . . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
2 | 1 | dmeqd 5248 | . 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵) |
3 | df-rn 5049 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
4 | df-rn 5049 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
5 | 2, 3, 4 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ◡ccnv 5037 dom cdm 5038 ran crn 5039 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-cnv 5046 df-dm 5048 df-rn 5049 |
This theorem is referenced by: rneqi 5273 rneqd 5274 feq1 5939 foeq1 6024 fnrnfv 6152 fconst5 6376 frxp 7174 tz7.44-2 7390 tz7.44-3 7391 ixpsnf1o 7834 ordtypecbv 8305 ordtypelem3 8308 dfac8alem 8735 dfac8a 8736 dfac5lem3 8831 dfac9 8841 dfac12lem1 8848 dfac12r 8851 ackbij2 8948 isfin3ds 9034 fin23lem17 9043 fin23lem29 9046 fin23lem30 9047 fin23lem32 9049 fin23lem34 9051 fin23lem35 9052 fin23lem39 9055 fin23lem41 9057 isf33lem 9071 isf34lem6 9085 dcomex 9152 axdc2lem 9153 zorn2lem1 9201 zorn2g 9208 ttukey2g 9221 gruurn 9499 rpnnen1lem6 11695 rpnnen1OLD 11701 relexp0g 13610 relexpsucnnr 13613 dfrtrcl2 13650 mpfrcl 19339 ply1frcl 19504 pnrmopn 20957 isi1f 23247 itg1val 23256 axlowdimlem13 25634 axlowdim1 25639 iscusgra 25985 isuvtx 26016 wwlk 26209 clwwlk 26294 rusgra0edg 26482 isfrgra 26517 ex-rn 26689 gidval 26750 grpoinvfval 26760 grpodivfval 26772 isablo 26784 vciOLD 26800 isvclem 26816 isnvlem 26849 isphg 27056 pj11i 27954 hmopidmch 28396 hmopidmpj 28397 pjss1coi 28406 padct 28885 locfinreflem 29235 locfinref 29236 issibf 29722 sitgfval 29730 mrsubvrs 30673 rdgprc0 30943 rdgprc 30944 dfrdg2 30945 brrangeg 31213 poimirlem24 32603 volsupnfl 32624 elghomlem1OLD 32854 isdivrngo 32919 iscom2 32964 dnnumch1 36632 aomclem3 36644 aomclem8 36649 rclexi 36941 rtrclex 36943 rtrclexi 36947 cnvrcl0 36951 dfrtrcl5 36955 dfrcl2 36985 csbima12gALTVD 38155 unirnmap 38395 ssmapsn 38403 sge0val 39259 vonvolmbl 39551 ausgrusgri 40398 0uhgrsubgr 40503 cusgrsize 40670 |
Copyright terms: Public domain | W3C validator |