Theorem cnvimarndm 6057

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 6044	. 2 ⊢ (◡𝐴 “ dom ◡𝐴) = ran ◡𝐴
2		df-rn 5652	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
3	2	imaeq2i 6032	. 2 ⊢ (◡𝐴 “ ran 𝐴) = (◡𝐴 “ dom ◡𝐴)
4		dfdm4 5862	. 2 ⊢ dom 𝐴 = ran ◡𝐴
5	1, 3, 4	3eqtr4i 2763	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

Syntax hints:   = wceq 1540  ^◡ccnv 5640  dom cdm 5641  ran crn 5642   “ cima 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  cnvimassrndm  6128  focnvimacdmdm  6787  cnvimainrn  7042  cnrest2  23180  mbfconstlem  25535  i1fima  25586  i1fima2  25587  i1fd  25589  i1f0rn  25590  itg1addlem5  25608  fcoinver  32540  supppreima  32621  sibfof  34338  itg2addnclem  37672  itg2addnclem2  37673  ftc1anclem6  37699  f1cof1blem  47079  f1cof1b  47082  fnfocofob  47084