Theorem cnvimarndm 6085

Description: The preimage of the range of a class is equal to the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.) (Proof shortened by BJ, 29-Sep-2026.)

Assertion

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

Proof of Theorem cnvimarndm

Step	Hyp	Ref	Expression
1		ssid 3934	. 2 ⊢ ran 𝐴 ⊆ ran 𝐴
2		cnvimassrndm 6084	. 2 ⊢ (ran 𝐴 ⊆ ran 𝐴 → (◡𝐴 “ ran 𝐴) = dom 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3899  ^◡ccnv 5653  dom cdm 5654  ran crn 5655   “ cima 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667

This theorem is used by:  cnvimassrndmOLD  6205  focnvimacdmdm  6816  cnvimainrn  7074  cnrest2  23616  mbfconstlem  25960  i1fima  26011  i1fima2  26012  i1fd  26014  i1f0rn  26015  itg1addlem5  26033  rnplynfin  26642  fcoinver  33252  supppreima  33338  sibfof  35025  itg2addnclem  38729  itg2addnclem2  38730  ftc1anclem6  38756  f1cof1blem  48283  f1cof1b  48286  fnfocofob  48288