Theorem fimacnv 6743

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3900  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658  ⟶wf 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fn 6550  df-f 6551

This theorem is used by:  fco  6745  f1co  6802  fimacnvinrn  7082  fmpt  7121  fsuppeq  8206  fsuppeqg  8207  fin1a2lem7  10497  cnclima  23601  iscncl  23602  cnindis  23625  cncmp  23725  ptrescn  23973  qtopuni  24036  qtopcld  24047  qtopcmap  24053  ordthmeolem  24135  rnelfmlem  24286  mbfdm  25962  ismbf  25964  mbfimaicc  25967  ismbf2d  25976  ismbf3d  25990  mbfimaopn2  25993  i1fd  26017  plyeq0  26545  elrspunidl  34034  fsumcvg4  34638  zrhunitpreima  34664  imambfm  34950  carsggect  35006  dstrvprob  35160  poimirlem30  38714  dvtan  38734  smfresal  47943  cnneiima  50176