| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cnvimarndm | Structured version Visualization version GIF version | ||
| Description: The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.) |
| Ref | Expression |
|---|---|
| cnvimarndm | ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imadmrn 6029 | . 2 ⊢ (◡𝐴 “ dom ◡𝐴) = ran ◡𝐴 | |
| 2 | df-rn 5635 | . . 3 ⊢ ran 𝐴 = dom ◡𝐴 | |
| 3 | 2 | imaeq2i 6017 | . 2 ⊢ (◡𝐴 “ ran 𝐴) = (◡𝐴 “ dom ◡𝐴) |
| 4 | dfdm4 5844 | . 2 ⊢ dom 𝐴 = ran ◡𝐴 | |
| 5 | 1, 3, 4 | 3eqtr4i 2769 | 1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1541 ◡ccnv 5623 dom cdm 5624 ran crn 5625 “ cima 5627 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-xp 5630 df-cnv 5632 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 |
| This theorem is referenced by: cnvimassrndm 6110 focnvimacdmdm 6758 cnvimainrn 7012 cnrest2 23230 mbfconstlem 25584 i1fima 25635 i1fima2 25636 i1fd 25638 i1f0rn 25639 itg1addlem5 25657 fcoinver 32679 supppreima 32770 sibfof 34497 itg2addnclem 37872 itg2addnclem2 37873 ftc1anclem6 37899 f1cof1blem 47330 f1cof1b 47333 fnfocofob 47335 |
| Copyright terms: Public domain | W3C validator |