Theorem cnvimarndm 6075

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 6062	. 2 ⊢ (◡𝐴 “ dom ◡𝐴) = ran ◡𝐴
2		df-rn 5670	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
3	2	imaeq2i 6050	. 2 ⊢ (◡𝐴 “ ran 𝐴) = (◡𝐴 “ dom ◡𝐴)
4		dfdm4 5880	. 2 ⊢ dom 𝐴 = ran ◡𝐴
5	1, 3, 4	3eqtr4i 2769	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

Syntax hints:   = wceq 1540  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   “ cima 5662

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  cnvimassrndm  6146  focnvimacdmdm  6807  cnvimainrn  7062  cnrest2  23229  mbfconstlem  25585  i1fima  25636  i1fima2  25637  i1fd  25639  i1f0rn  25640  itg1addlem5  25658  fcoinver  32590  supppreima  32673  sibfof  34377  itg2addnclem  37700  itg2addnclem2  37701  ftc1anclem6  37727  f1cof1blem  47070  f1cof1b  47073  fnfocofob  47075