Theorem imaeq2 6058

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 5973	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5928	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5674	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5674	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674

This theorem is referenced by:  imaeq2i  6060  imaeq2d  6062  relimasn  6087  cnvimassrndm  6149  fimadmfo  6801  ssimaex  6966  ssimaexg  6967  isoselem  7339  isowe2  7348  f1opw2  7665  mptcnfimad  7979  fnse  8125  supp0cosupp0  8200  tz7.49  8428  ecexr  8695  fopwdom  9069  sbthlem2  9072  sbth  9081  ssenen  9135  sbthfi  9179  fodomfi  9268  domunfican  9277  f1opwfi  9309  fipreima  9311  marypha1lem  9389  ordtypelem2  9477  ordtypelem3  9478  ordtypelem9  9484  dfac12lem2  10124  dfac12r  10126  ackbij2lem2  10218  ackbij2lem3  10219  r1om  10222  enfin2i  10300  zorn2lem6  10480  zorn2lem7  10481  isacs5lem  18596  acsdrscl  18597  gicsubgen  19344  ghmqusnsglem1  19345  ghmquskerlem1  19348  ghmquskerco  19349  gicqusker  19353  efgrelexlema  19814  tgcn  23409  subbascn  23411  iscnp4  23420  cnpnei  23421  cnima  23422  iscncl  23426  cncls  23431  cnconst2  23440  cnrest2  23443  cnprest  23446  cnindis  23449  cncmp  23549  cmpfi  23565  2ndcomap  23615  ptbasfi  23738  xkoopn  23746  xkoccn  23776  txcnp  23777  ptcnplem  23778  txcnmpt  23781  ptrescn  23796  xkoco1cn  23814  xkoco2cn  23815  xkococn  23817  xkoinjcn  23844  elqtop  23854  qtopomap  23875  qtopcmap  23876  ordthmeolem  23958  fbasrn  24041  elfm  24104  elfm2  24105  elfm3  24107  imaelfm  24108  rnelfmlem  24109  rnelfm  24110  fmfnfmlem2  24112  fmfnfmlem3  24113  fmfnfmlem4  24114  fmco  24118  flffbas  24152  lmflf  24162  fcfneii  24194  ptcmplem3  24211  ptcmplem5  24213  ptcmpg  24214  cnextcn  24224  symgtgp  24263  ghmcnp  24272  eltsms  24290  tsmsf1o  24302  fmucnd  24448  ucnextcn  24460  metcnp3  24697  mbfdm  25785  ismbf  25787  mbfima  25789  ismbfd  25798  mbfimaopnlem  25814  mbfimaopn2  25816  i1fd  25840  ellimc2  26036  limcflf  26040  xrlimcnp  27133  oldval  28027  ubthlem1  31222  disjpreima  32929  imadifxp  32946  preimane  33014  fnpreimac  33015  lmicqusker  33727  ricqusker  33735  algextdeglem4  34110  algextdeg  34115  qtophaus  34226  rhmpreimacnlem  34274  rrhre  34411  mbfmcnvima  34645  imambfm  34652  eulerpartgbij  34762  erdszelem1  35683  erdsze  35694  erdsze2lem2  35696  cvmscbv  35750  cvmsi  35757  cvmsval  35758  cvmliftlem15  35790  opelco3  36267  brimageg  36417  fnimage  36419  imageval  36420  fvimage  36421  filnetlem4  36892  bj-imdirval3  37828  bj-imdirco  37834  ptrest  38270  ismtyhmeolem  38455  ismtybndlem  38457  heibor1lem  38460  zndvdchrrhm  42740  aks6d1c7lem2  42948  aks5lem4a  42957  lmhmfgima  43811  brtrclfv2  44453  csbfv12gALTVD  45607  icccncfext  46601  sge0f1o  47096  smfresal  47502  smfpimbor1lem1  47512  smfpimbor1lem2  47513  smfco  47516  f1cof1b  47814  fnfocofob  47816  imaelsetpreimafv  48144  fundcmpsurinjlem3  48149  imasetpreimafvbijlemfo  48154  fundcmpsurbijinjpreimafv  48156  grimco  48654  uhgrimedgi  48655  isuspgrim0  48659  isuspgrimlem  48660  upgrimwlklem5  48666  gricushgr  48682  grimedg  48700  grtrimap  48713  isubgr3stgrlem5  48735  isubgr3stgrlem6  48736  isubgr3stgrlem7  48737  isubgr3stgrlem8  48738  uspgrlimlem4  48756  grlimedgclnbgr  48760  grlimgrtrilem2  48767