Theorem fimacnv 6694

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 6679	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
2		cnvimassrndm 6120	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹)
3	1, 2	syl 17	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹)
4		fdm 6681	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
5	3, 4	eqtrd 2772	1 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903  ^◡ccnv 5633  dom cdm 5634  ran crn 5635   “ cima 5637  ⟶wf 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5640  df-cnv 5642  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fn 6505  df-f 6506

This theorem is referenced by:  fco  6696  f1co  6751  fimacnvinrn  7027  fmpt  7066  fsuppeq  8129  fsuppeqg  8130  fin1a2lem7  10330  cnclima  23229  iscncl  23230  cnindis  23253  cncmp  23353  ptrescn  23600  qtopuni  23663  qtopcld  23674  qtopcmap  23680  ordthmeolem  23762  rnelfmlem  23913  mbfdm  25600  ismbf  25602  mbfimaicc  25605  ismbf2d  25614  ismbf3d  25628  mbfimaopn2  25631  i1fd  25655  plyeq0  26189  elrspunidl  33527  fsumcvg4  34134  zrhunitpreima  34160  imambfm  34446  carsggect  34502  dstrvprob  34656  poimirlem30  37930  dvtan  37950  smfresal  47175  cnneiima  49305