Theorem fimacnv 6716

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

Syntax hints:   → wi 4   = wceq 1562   ⊆ wss 3906  ^◡ccnv 5648  dom cdm 5649  ran crn 5650   “ cima 5652  ⟶wf 6519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-xp 5655  df-cnv 5657  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-fn 6526  df-f 6527

This theorem is referenced by:  fco  6718  f1co  6775  fimacnvinrn  7054  fmpt  7093  fsuppeq  8157  fsuppeqg  8158  fin1a2lem7  10365  cnclima  23330  iscncl  23331  cnindis  23354  cncmp  23454  ptrescn  23701  qtopuni  23764  qtopcld  23775  qtopcmap  23781  ordthmeolem  23863  rnelfmlem  24014  mbfdm  25690  ismbf  25692  mbfimaicc  25695  ismbf2d  25704  ismbf3d  25718  mbfimaopn2  25721  i1fd  25745  plyeq0  26273  elrspunidl  33616  fsumcvg4  34249  zrhunitpreima  34275  imambfm  34561  carsggect  34617  dstrvprob  34771  poimirlem30  38154  dvtan  38174  smfresal  47367  cnneiima  49543