Theorem imaeq2 5381

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq2	⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 5312	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5274	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5051	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5051	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1475  ran crn 5039   ↾ cres 5040   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  imaeq2i  5383  imaeq2d  5385  relimasn  5407  funimaexg  5889  ssimaex  6173  ssimaexg  6174  isoselem  6491  isowe2  6500  f1opw2  6786  fnse  7181  supp0cosupp0  7221  tz7.49  7427  ecexr  7634  fopwdom  7953  sbthlem2  7956  sbth  7965  ssenen  8019  domunfican  8118  fodomfi  8124  f1opwfi  8153  fipreima  8155  marypha1lem  8222  ordtypelem2  8307  ordtypelem3  8308  ordtypelem9  8314  dfac12lem2  8849  dfac12r  8851  ackbij2lem2  8945  ackbij2lem3  8946  r1om  8949  enfin2i  9026  zorn2lem6  9206  zorn2lem7  9207  isacs5lem  16992  acsdrscl  16993  gicsubgen  17544  efgrelexlema  17985  tgcn  20866  subbascn  20868  iscnp4  20877  cnpnei  20878  cnima  20879  iscncl  20883  cncls  20888  cnconst2  20897  cnrest2  20900  cnprest  20903  cnindis  20906  cncmp  21005  cmpfi  21021  2ndcomap  21071  ptbasfi  21194  xkoopn  21202  xkoccn  21232  txcnp  21233  ptcnplem  21234  txcnmpt  21237  ptrescn  21252  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  elqtop  21310  qtopomap  21331  qtopcmap  21332  ordthmeolem  21414  fbasrn  21498  elfm  21561  elfm2  21562  elfm3  21564  imaelfm  21565  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem3  21570  fmfnfmlem4  21571  fmco  21575  flffbas  21609  lmflf  21619  fcfneii  21651  ptcmplem3  21668  ptcmplem5  21670  ptcmpg  21671  cnextcn  21681  symgtgp  21715  ghmcnp  21728  eltsms  21746  tsmsf1o  21758  fmucnd  21906  ucnextcn  21918  metcnp3  22155  mbfdm  23201  ismbf  23203  mbfima  23205  ismbfd  23213  mbfimaopnlem  23228  mbfimaopn2  23230  i1fd  23254  ellimc2  23447  limcflf  23451  xrlimcnp  24495  ubthlem1  27110  disjpreima  28779  imadifxp  28796  qtophaus  29231  rrhre  29393  mbfmcnvima  29646  imambfm  29651  eulerpartgbij  29761  erdszelem1  30427  erdsze  30438  erdsze2lem2  30440  cvmscbv  30494  cvmsi  30501  cvmsval  30502  cvmliftlem15  30534  opelco3  30923  brimageg  31204  fnimage  31206  imageval  31207  fvimage  31208  filnetlem4  31546  ptrest  32578  ismtyhmeolem  32773  ismtybndlem  32775  heibor1lem  32778  lmhmfgima  36672  brtrclfv2  37038  csbfv12gALTVD  38157  icccncfext  38773  sge0f1o  39275  smfresal  39673  smfpimbor1lem1  39683  smfpimbor1lem2  39684  smfco  39687