Theorem fimacnv 6622

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887  ^◡ccnv 5588  dom cdm 5589  ran crn 5590   “ cima 5592  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-fn 6436  df-f 6437

This theorem is referenced by:  fco  6624  f1co  6682  fimacnvinrn  6949  fmpt  6984  frnsuppeq  7991  frnsuppeqg  7992  fin1a2lem7  10162  cnclima  22419  iscncl  22420  cnindis  22443  cncmp  22543  ptrescn  22790  qtopuni  22853  qtopcld  22864  qtopcmap  22870  ordthmeolem  22952  rnelfmlem  23103  mbfdm  24790  ismbf  24792  mbfimaicc  24795  ismbf2d  24804  ismbf3d  24818  mbfimaopn2  24821  i1fd  24845  plyeq0  25372  elrspunidl  31606  fsumcvg4  31900  zrhunitpreima  31928  imambfm  32229  carsggect  32285  dstrvprob  32438  poimirlem30  35807  dvtan  35827  smfresal  44322  cnneiima  46210