Theorem imaeq2 5968

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 5889	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5850	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5603	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5603	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1539  ran crn 5591   ↾ cres 5592   “ cima 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603

This theorem is referenced by:  imaeq2i  5970  imaeq2d  5972  relimasn  5995  cnvimassrndm  6060  funimaexgOLD  6528  fimadmfo  6706  ssimaex  6862  ssimaexg  6863  isoselem  7221  isowe2  7230  f1opw2  7533  fnse  7983  supp0cosupp0  8033  tz7.49  8285  ecexr  8512  fopwdom  8876  sbthlem2  8880  sbth  8889  ssenen  8947  imafi  8967  sbthfi  8994  domunfican  9096  fodomfi  9101  f1opwfi  9132  fipreima  9134  marypha1lem  9201  ordtypelem2  9287  ordtypelem3  9288  ordtypelem9  9294  dfac12lem2  9909  dfac12r  9911  ackbij2lem2  10005  ackbij2lem3  10006  r1om  10009  enfin2i  10086  zorn2lem6  10266  zorn2lem7  10267  isacs5lem  18272  acsdrscl  18273  gicsubgen  18903  efgrelexlema  19364  tgcn  22412  subbascn  22414  iscnp4  22423  cnpnei  22424  cnima  22425  iscncl  22429  cncls  22434  cnconst2  22443  cnrest2  22446  cnprest  22449  cnindis  22452  cncmp  22552  cmpfi  22568  2ndcomap  22618  ptbasfi  22741  xkoopn  22749  xkoccn  22779  txcnp  22780  ptcnplem  22781  txcnmpt  22784  ptrescn  22799  xkoco1cn  22817  xkoco2cn  22818  xkococn  22820  xkoinjcn  22847  elqtop  22857  qtopomap  22878  qtopcmap  22879  ordthmeolem  22961  fbasrn  23044  elfm  23107  elfm2  23108  elfm3  23110  imaelfm  23111  rnelfmlem  23112  rnelfm  23113  fmfnfmlem2  23115  fmfnfmlem3  23116  fmfnfmlem4  23117  fmco  23121  flffbas  23155  lmflf  23165  fcfneii  23197  ptcmplem3  23214  ptcmplem5  23216  ptcmpg  23217  cnextcn  23227  symgtgp  23266  ghmcnp  23275  eltsms  23293  tsmsf1o  23305  fmucnd  23453  ucnextcn  23465  metcnp3  23705  mbfdm  24799  ismbf  24801  mbfima  24803  ismbfd  24812  mbfimaopnlem  24828  mbfimaopn2  24830  i1fd  24854  ellimc2  25050  limcflf  25054  xrlimcnp  26127  ubthlem1  29241  disjpreima  30932  imadifxp  30949  preimane  31016  fnpreimac  31017  qtophaus  31795  rhmpreimacnlem  31843  rrhre  31980  mbfmcnvima  32233  imambfm  32238  eulerpartgbij  32348  erdszelem1  33162  erdsze  33173  erdsze2lem2  33175  cvmscbv  33229  cvmsi  33236  cvmsval  33237  cvmliftlem15  33269  opelco3  33758  oldval  34047  brimageg  34238  fnimage  34240  imageval  34241  fvimage  34242  filnetlem4  34579  bj-imdirval3  35364  bj-imdirco  35370  ptrest  35785  ismtyhmeolem  35971  ismtybndlem  35973  heibor1lem  35976  lmhmfgima  40916  brtrclfv2  41342  csbfv12gALTVD  42526  icccncfext  43435  sge0f1o  43927  smfresal  44333  smfpimbor1lem1  44343  smfpimbor1lem2  44344  smfco  44347  f1cof1b  44580  fnfocofob  44582  imaelsetpreimafv  44858  fundcmpsurinjlem3  44863  imasetpreimafvbijlemfo  44868  fundcmpsurbijinjpreimafv  44870  isomushgr  45289  isomuspgrlem1  45290  isomuspgrlem2a  45291  isomuspgrlem2b  45292  isomuspgrlem2c  45293  isomuspgrlem2d  45294  isomuspgr  45297  isomgrsym  45299