Theorem cnvimarndm 6079

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 6066	. 2 ⊢ (◡𝐴 “ dom ◡𝐴) = ran ◡𝐴
2		df-rn 5666	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
3	2	imaeq2i 6054	. 2 ⊢ (◡𝐴 “ ran 𝐴) = (◡𝐴 “ dom ◡𝐴)
4		dfdm4 5879	. 2 ⊢ dom 𝐴 = ran ◡𝐴
5	1, 3, 4	3eqtr4i 2793	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

This proof depends on syntax axioms:   = wceq 1570  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  cnvimassrndm  6143  focnvimacdmdm  6802  cnvimainrn  7060  cnrest2  23514  mbfconstlem  25858  i1fima  25909  i1fima2  25910  i1fd  25912  i1f0rn  25913  itg1addlem5  25931  rnplynfin  26542  fcoinver  33080  supppreima  33166  sibfof  34854  itg2addnclem  38423  itg2addnclem2  38424  ftc1anclem6  38450  f1cof1blem  47965  f1cof1b  47968  fnfocofob  47970