Theorem fimacnv 6681

Description: The preimage of the codomain of a function is the function's domain. (Contributed by FL, 25-Jan-2007.) (Proof shortened by AV, 20-Sep-2024.)

Assertion

Ref	Expression
fimacnv	⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)

Proof of Theorem fimacnv

Step	Hyp	Ref	Expression
1		frn 6666	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
2		cnvimassrndm 6107	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹)
3	1, 2	syl 17	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹)
4		fdm 6668	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
5	3, 4	eqtrd 2776	1 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1548   ⊆ wss 3885  ^◡ccnv 5620  dom cdm 5621  ran crn 5622   “ cima 5624  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fn 6492  df-f 6493

This theorem is referenced by:  fco  6683  f1co  6738  fimacnvinrn  7016  fmpt  7055  fsuppeq  8119  fsuppeqg  8120  fin1a2lem7  10323  cnclima  23255  iscncl  23256  cnindis  23279  cncmp  23379  ptrescn  23626  qtopuni  23689  qtopcld  23700  qtopcmap  23706  ordthmeolem  23788  rnelfmlem  23939  mbfdm  25615  ismbf  25617  mbfimaicc  25620  ismbf2d  25629  ismbf3d  25643  mbfimaopn2  25646  i1fd  25670  plyeq0  26198  elrspunidl  33515  fsumcvg4  34146  zrhunitpreima  34172  imambfm  34458  carsggect  34514  dstrvprob  34668  poimirlem30  38032  dvtan  38052  smfresal  47245  cnneiima  49421