Theorem fimacnv 6713

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917  ^◡ccnv 5640  dom cdm 5641  ran crn 5642   “ cima 5644  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fn 6517  df-f 6518

This theorem is referenced by:  fco  6715  f1co  6770  fimacnvinrn  7046  fmpt  7085  fsuppeq  8157  fsuppeqg  8158  fin1a2lem7  10366  cnclima  23162  iscncl  23163  cnindis  23186  cncmp  23286  ptrescn  23533  qtopuni  23596  qtopcld  23607  qtopcmap  23613  ordthmeolem  23695  rnelfmlem  23846  mbfdm  25534  ismbf  25536  mbfimaicc  25539  ismbf2d  25548  ismbf3d  25562  mbfimaopn2  25565  i1fd  25589  plyeq0  26123  elrspunidl  33406  fsumcvg4  33947  zrhunitpreima  33973  imambfm  34260  carsggect  34316  dstrvprob  34470  poimirlem30  37651  dvtan  37671  smfresal  46793  cnneiima  48909