Theorem imaeq2 6021

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 5939	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5893	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5644	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5644	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1542  ran crn 5632   ↾ cres 5633   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq2i  6023  imaeq2d  6025  relimasn  6050  cnvimassrndm  6116  fimadmfo  6761  ssimaex  6925  ssimaexg  6926  isoselem  7296  isowe2  7305  f1opw2  7622  mptcnfimad  7939  fnse  8083  supp0cosupp0  8158  tz7.49  8384  ecexr  8648  fopwdom  9023  sbthlem2  9026  sbth  9035  ssenen  9089  sbthfi  9133  fodomfi  9222  imafiOLD  9226  domunfican  9232  fodomfiOLD  9240  f1opwfi  9266  fipreima  9268  marypha1lem  9346  ordtypelem2  9434  ordtypelem3  9435  ordtypelem9  9441  dfac12lem2  10067  dfac12r  10069  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  enfin2i  10243  zorn2lem6  10423  zorn2lem7  10424  isacs5lem  18511  acsdrscl  18512  gicsubgen  19254  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmquskerco  19259  gicqusker  19263  efgrelexlema  19724  tgcn  23217  subbascn  23219  iscnp4  23228  cnpnei  23229  cnima  23230  iscncl  23234  cncls  23239  cnconst2  23248  cnrest2  23251  cnprest  23254  cnindis  23257  cncmp  23357  cmpfi  23373  2ndcomap  23423  ptbasfi  23546  xkoopn  23554  xkoccn  23584  txcnp  23585  ptcnplem  23586  txcnmpt  23589  ptrescn  23604  xkoco1cn  23622  xkoco2cn  23623  xkococn  23625  xkoinjcn  23652  elqtop  23662  qtopomap  23683  qtopcmap  23684  ordthmeolem  23766  fbasrn  23849  elfm  23912  elfm2  23913  elfm3  23915  imaelfm  23916  rnelfmlem  23917  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem3  23921  fmfnfmlem4  23922  fmco  23926  flffbas  23960  lmflf  23970  fcfneii  24002  ptcmplem3  24019  ptcmplem5  24021  ptcmpg  24022  cnextcn  24032  symgtgp  24071  ghmcnp  24080  eltsms  24098  tsmsf1o  24110  fmucnd  24256  ucnextcn  24268  metcnp3  24505  mbfdm  25593  ismbf  25595  mbfima  25597  ismbfd  25606  mbfimaopnlem  25622  mbfimaopn2  25624  i1fd  25648  ellimc2  25844  limcflf  25848  xrlimcnp  26932  oldval  27826  ubthlem1  30941  disjpreima  32654  imadifxp  32671  preimane  32742  fnpreimac  32743  lmicqusker  33478  ricqusker  33487  algextdeglem4  33864  algextdeg  33869  qtophaus  33980  rhmpreimacnlem  34028  rrhre  34165  mbfmcnvima  34399  imambfm  34406  eulerpartgbij  34516  erdszelem1  35373  erdsze  35384  erdsze2lem2  35386  cvmscbv  35440  cvmsi  35447  cvmsval  35448  cvmliftlem15  35480  opelco3  35957  brimageg  36107  fnimage  36109  imageval  36110  fvimage  36111  filnetlem4  36563  bj-imdirval3  37498  bj-imdirco  37504  ptrest  37940  ismtyhmeolem  38125  ismtybndlem  38127  heibor1lem  38130  zndvdchrrhm  42412  aks6d1c7lem2  42620  aks5lem4a  42629  lmhmfgima  43512  brtrclfv2  44154  csbfv12gALTVD  45325  icccncfext  46315  sge0f1o  46810  smfresal  47216  smfpimbor1lem1  47226  smfpimbor1lem2  47227  smfco  47230  f1cof1b  47525  fnfocofob  47527  imaelsetpreimafv  47855  fundcmpsurinjlem3  47860  imasetpreimafvbijlemfo  47865  fundcmpsurbijinjpreimafv  47867  grimco  48365  uhgrimedgi  48366  isuspgrim0  48370  isuspgrimlem  48371  upgrimwlklem5  48377  gricushgr  48393  grimedg  48411  grtrimap  48424  isubgr3stgrlem5  48446  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  isubgr3stgrlem8  48449  uspgrlimlem4  48467  grlimedgclnbgr  48471  grlimgrtrilem2  48478