Theorem cnvimarndm 6008

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 5997	. 2 ⊢ (◡𝐴 “ dom ◡𝐴) = ran ◡𝐴
2		df-rn 5619	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
3	2	imaeq2i 5985	. 2 ⊢ (◡𝐴 “ ran 𝐴) = (◡𝐴 “ dom ◡𝐴)
4		dfdm4 5825	. 2 ⊢ dom 𝐴 = ran ◡𝐴
5	1, 3, 4	3eqtr4i 2775	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

Syntax hints:   = wceq 1540  ^◡ccnv 5607  dom cdm 5608  ran crn 5609   “ cima 5611

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-br 5088  df-opab 5150  df-xp 5614  df-cnv 5616  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621

This theorem is referenced by:  cnvimassrndm  6078  focnvimacdmdm  6738  cnvimainrn  6984  cnrest2  22520  mbfconstlem  24874  i1fima  24925  i1fima2  24926  i1fd  24928  i1f0rn  24929  itg1addlem5  24948  fcoinver  31081  supppreima  31160  sibfof  32447  itg2addnclem  35900  itg2addnclem2  35901  ftc1anclem6  35927  f1cof1blem  44833  f1cof1b  44834  fnfocofob  44836