Theorem cnvimarndm 6035

Description: The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.)

Assertion

Ref	Expression
cnvimarndm	⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

Proof of Theorem cnvimarndm

Step	Hyp	Ref	Expression
1		imadmrn 6022	. 2 ⊢ (◡𝐴 “ dom ◡𝐴) = ran ◡𝐴
2		df-rn 5629	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
3	2	imaeq2i 6010	. 2 ⊢ (◡𝐴 “ ran 𝐴) = (◡𝐴 “ dom ◡𝐴)
4		dfdm4 5837	. 2 ⊢ dom 𝐴 = ran ◡𝐴
5	1, 3, 4	3eqtr4i 2772	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

Syntax hints:   = wceq 1547  ^◡ccnv 5617  dom cdm 5618  ran crn 5619   “ cima 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  cnvimassrndm  6103  focnvimacdmdm  6751  cnvimainrn  7008  cnrest2  23269  mbfconstlem  25612  i1fima  25663  i1fima2  25664  i1fd  25666  i1f0rn  25667  itg1addlem5  25685  fcoinver  32693  supppreima  32783  sibfof  34524  itg2addnclem  38038  itg2addnclem2  38039  ftc1anclem6  38065  f1cof1blem  47537  f1cof1b  47540  fnfocofob  47542