Theorem fimacnv 6732

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899  ^◡ccnv 5650  dom cdm 5651  ran crn 5652   “ cima 5654  ⟶wf 6534

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fn 6541  df-f 6542

This theorem is used by:  fco  6734  f1co  6791  fimacnvinrn  7071  fmpt  7110  fsuppeq  8192  fsuppeqg  8193  fin1a2lem7  10484  cnclima  23586  iscncl  23587  cnindis  23610  cncmp  23710  ptrescn  23958  qtopuni  24021  qtopcld  24032  qtopcmap  24038  ordthmeolem  24120  rnelfmlem  24271  mbfdm  25947  ismbf  25949  mbfimaicc  25952  ismbf2d  25961  ismbf3d  25975  mbfimaopn2  25978  i1fd  26002  plyeq0  26530  elrspunidl  33978  fsumcvg4  34582  zrhunitpreima  34608  imambfm  34894  carsggect  34950  dstrvprob  35104  poimirlem30  38568  dvtan  38588  smfresal  47797  cnneiima  50024