Theorem cnvimarndm 6098

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 3935	. 2 ⊢ ran 𝐴 ⊆ ran 𝐴
2		cnvimassrndm 6097	. 2 ⊢ (ran 𝐴 ⊆ ran 𝐴 → (◡𝐴 “ ran 𝐴) = dom 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3900  ^◡ccnv 5657  dom cdm 5658  ran crn 5659   “ cima 5661

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671

This theorem is used by:  cnvimassrndmOLD  6218  focnvimacdmdm  6838  cnvimainrn  7098  cnrest2  23659  mbfconstlem  26003  i1fima  26054  i1fima2  26055  i1fd  26057  i1f0rn  26058  itg1addlem5  26076  rnplynfin  26685  fcoinver  33296  supppreima  33381  sibfof  35083  itg2addnclem  38857  itg2addnclem2  38858  ftc1anclem6  38884  f1cof1blem  48417  f1cof1b  48420  fnfocofob  48422