Theorem imaeq2 6059

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 5974	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5929	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5675	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5675	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2829	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1567  ran crn 5663   ↾ cres 5664   “ cima 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  imaeq2i  6061  imaeq2d  6063  relimasn  6088  cnvimassrndm  6150  fimadmfo  6802  ssimaex  6967  ssimaexg  6968  isoselem  7340  isowe2  7349  f1opw2  7666  mptcnfimad  7982  fnse  8128  supp0cosupp0  8203  tz7.49  8431  ecexr  8698  fopwdom  9072  sbthlem2  9075  sbth  9084  ssenen  9138  sbthfi  9182  fodomfi  9271  domunfican  9280  f1opwfi  9312  fipreima  9314  marypha1lem  9392  ordtypelem2  9480  ordtypelem3  9481  ordtypelem9  9487  dfac12lem2  10127  dfac12r  10129  ackbij2lem2  10221  ackbij2lem3  10222  r1om  10225  enfin2i  10304  zorn2lem6  10484  zorn2lem7  10485  isacs5lem  18600  acsdrscl  18601  gicsubgen  19348  ghmqusnsglem1  19349  ghmquskerlem1  19352  ghmquskerco  19353  gicqusker  19357  efgrelexlema  19818  tgcn  23377  subbascn  23379  iscnp4  23388  cnpnei  23389  cnima  23390  iscncl  23394  cncls  23399  cnconst2  23408  cnrest2  23411  cnprest  23414  cnindis  23417  cncmp  23517  cmpfi  23533  2ndcomap  23583  ptbasfi  23706  xkoopn  23714  xkoccn  23744  txcnp  23745  ptcnplem  23746  txcnmpt  23749  ptrescn  23764  xkoco1cn  23782  xkoco2cn  23783  xkococn  23785  xkoinjcn  23812  elqtop  23822  qtopomap  23843  qtopcmap  23844  ordthmeolem  23926  fbasrn  24009  elfm  24072  elfm2  24073  elfm3  24075  imaelfm  24076  rnelfmlem  24077  rnelfm  24078  fmfnfmlem2  24080  fmfnfmlem3  24081  fmfnfmlem4  24082  fmco  24086  flffbas  24120  lmflf  24130  fcfneii  24162  ptcmplem3  24179  ptcmplem5  24181  ptcmpg  24182  cnextcn  24192  symgtgp  24231  ghmcnp  24240  eltsms  24258  tsmsf1o  24270  fmucnd  24416  ucnextcn  24428  metcnp3  24665  mbfdm  25753  ismbf  25755  mbfima  25757  ismbfd  25766  mbfimaopnlem  25782  mbfimaopn2  25784  i1fd  25808  ellimc2  26004  limcflf  26008  xrlimcnp  27098  oldval  27992  ubthlem1  31162  disjpreima  32869  imadifxp  32886  preimane  32954  fnpreimac  32955  lmicqusker  33670  ricqusker  33678  algextdeglem4  34054  algextdeg  34059  qtophaus  34170  rhmpreimacnlem  34218  rrhre  34355  mbfmcnvima  34589  imambfm  34596  eulerpartgbij  34706  erdszelem1  35581  erdsze  35592  erdsze2lem2  35594  cvmscbv  35648  cvmsi  35655  cvmsval  35656  cvmliftlem15  35688  opelco3  36165  brimageg  36315  fnimage  36317  imageval  36318  fvimage  36319  filnetlem4  36780  bj-imdirval3  37715  bj-imdirco  37721  ptrest  38157  ismtyhmeolem  38342  ismtybndlem  38344  heibor1lem  38347  zndvdchrrhm  42629  aks6d1c7lem2  42837  aks5lem4a  42846  lmhmfgima  43702  brtrclfv2  44344  csbfv12gALTVD  45498  icccncfext  46492  sge0f1o  46987  smfresal  47393  smfpimbor1lem1  47403  smfpimbor1lem2  47404  smfco  47407  f1cof1b  47702  fnfocofob  47704  imaelsetpreimafv  48032  fundcmpsurinjlem3  48037  imasetpreimafvbijlemfo  48042  fundcmpsurbijinjpreimafv  48044  grimco  48542  uhgrimedgi  48543  isuspgrim0  48547  isuspgrimlem  48548  upgrimwlklem5  48554  gricushgr  48570  grimedg  48588  grtrimap  48601  isubgr3stgrlem5  48623  isubgr3stgrlem6  48624  isubgr3stgrlem7  48625  isubgr3stgrlem8  48626  uspgrlimlem4  48644  grlimedgclnbgr  48648  grlimgrtrilem2  48655