![]() |
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 5451 | . . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | |
2 | 1 | dmeqd 5481 | . 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵) |
3 | df-rn 5277 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
4 | df-rn 5277 | . 2 ⊢ ran 𝐵 = dom ◡𝐵 | |
5 | 2, 3, 4 | 3eqtr4g 2819 | 1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ◡ccnv 5265 dom cdm 5266 ran crn 5267 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-br 4805 df-opab 4865 df-cnv 5274 df-dm 5276 df-rn 5277 |
This theorem is referenced by: rneqi 5507 rneqd 5508 feq1 6187 foeq1 6272 fnrnfv 6404 fconst5 6635 frxp 7455 tz7.44-2 7672 tz7.44-3 7673 ixpsnf1o 8114 ordtypecbv 8587 ordtypelem3 8590 dfac8alem 9042 dfac8a 9043 dfac5lem3 9138 dfac9 9150 dfac12lem1 9157 dfac12r 9160 ackbij2 9257 isfin3ds 9343 fin23lem17 9352 fin23lem29 9355 fin23lem30 9356 fin23lem32 9358 fin23lem34 9360 fin23lem35 9361 fin23lem39 9364 fin23lem41 9366 isf33lem 9380 isf34lem6 9394 dcomex 9461 axdc2lem 9462 zorn2lem1 9510 zorn2g 9517 ttukey2g 9530 gruurn 9812 rpnnen1lem6 12012 rpnnen1OLD 12018 relexp0g 13961 relexpsucnnr 13964 dfrtrcl2 14001 mpfrcl 19720 ply1frcl 19885 pnrmopn 21349 isi1f 23640 itg1val 23649 axlowdimlem13 26033 axlowdim1 26038 ausgrusgri 26262 0uhgrsubgr 26370 cusgrsize 26560 ex-rn 27608 gidval 27675 grpoinvfval 27685 grpodivfval 27697 isablo 27709 vciOLD 27725 isvclem 27741 isnvlem 27774 isphg 27981 pj11i 28879 hmopidmch 29321 hmopidmpj 29322 pjss1coi 29331 padct 29806 locfinreflem 30216 locfinref 30217 issibf 30704 sitgfval 30712 mrsubvrs 31726 rdgprc0 32004 rdgprc 32005 dfrdg2 32006 madeval 32241 brrangeg 32349 poimirlem24 33746 volsupnfl 33767 elghomlem1OLD 33997 isdivrngo 34062 iscom2 34107 elrefrels2 34590 elrefrels3 34591 refreleq 34593 elcnvrefrels2 34603 elcnvrefrels3 34604 dnnumch1 38116 aomclem3 38128 aomclem8 38133 rclexi 38424 rtrclex 38426 rtrclexi 38430 cnvrcl0 38434 dfrtrcl5 38438 dfrcl2 38468 csbima12gALTVD 39632 unirnmap 39899 ssmapsn 39907 sge0val 41086 vonvolmbl 41381 |
Copyright terms: Public domain | W3C validator |