Theorem fimacnv 6727

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 6712	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
2		cnvimassrndm 6144	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹)
3	1, 2	syl 18	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹)
4		fdm 6714	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
5	3, 4	eqtrd 2795	1 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658  ⟶wf 6530

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  df-fn 6537  df-f 6538

This theorem is used by:  fco  6729  f1co  6786  fimacnvinrn  7066  fmpt  7105  fsuppeq  8175  fsuppeqg  8176  fin1a2lem7  10430  cnclima  23522  iscncl  23523  cnindis  23546  cncmp  23646  ptrescn  23894  qtopuni  23957  qtopcld  23968  qtopcmap  23974  ordthmeolem  24056  rnelfmlem  24207  mbfdm  25883  ismbf  25885  mbfimaicc  25888  ismbf2d  25897  ismbf3d  25911  mbfimaopn2  25914  i1fd  25938  plyeq0  26466  elrspunidl  33886  fsumcvg4  34490  zrhunitpreima  34516  imambfm  34803  carsggect  34859  dstrvprob  35013  poimirlem30  38413  dvtan  38433  smfresal  47630  cnneiima  49857