Theorem imaeq2 6050

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 5966	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5921	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5664	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5664	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ran crn 5652   ↾ cres 5653   “ cima 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  imaeq2i  6052  imaeq2d  6054  relimasn  6085  cnvimassrndmOLD  6202  fimadmfo  6810  ssimaex  6975  ssimaexg  6976  isoselem  7353  isowe2  7362  f1opw2  7680  mptcnfimad  8002  fnse  8156  supp0cosupp0  8232  tz7.49  8462  ecexr  8729  fopwdom  9111  sbthlem2  9114  sbth  9123  ssenen  9177  sbthfi  9221  fodomfi  9311  domunfican  9320  f1opwfi  9352  fipreima  9354  marypha1lem  9432  ordtypelem2  9520  ordtypelem3  9521  ordtypelem9  9527  dfac12lem2  10230  dfac12r  10232  ackbij2lem2  10324  ackbij2lem3  10325  hfom  10328  enfin2i  10406  zorn2lem6  10586  zorn2lem7  10587  isacs5lem  18728  acsdrscl  18729  gicsubgen  19502  ghmqusnsglem1  19503  ghmquskerlem1  19506  ghmquskerco  19507  gicqusker  19511  efgrelexlema  19972  tgcn  23579  subbascn  23581  iscnp4  23590  cnpnei  23591  cnima  23592  iscncl  23596  cncls  23601  cnconst2  23610  cnrest2  23613  cnprest  23616  cnindis  23619  cncmp  23719  cmpfi  23735  2ndcomap  23786  ptbasfi  23909  xkoopn  23917  xkoccn  23947  txcnp  23948  ptcnplem  23949  txcnmpt  23952  ptrescn  23967  xkoco1cn  23985  xkoco2cn  23986  xkococn  23988  xkoinjcn  24015  elqtop  24025  qtopomap  24046  qtopcmap  24047  ordthmeolem  24129  fbasrn  24212  elfm  24275  elfm2  24276  elfm3  24278  imaelfm  24279  rnelfmlem  24280  rnelfm  24281  fmfnfmlem2  24283  fmfnfmlem3  24284  fmfnfmlem4  24285  fmco  24289  flffbas  24323  lmflf  24333  fcfneii  24365  ptcmplem3  24382  ptcmplem5  24384  ptcmpg  24385  cnextcn  24395  symgtgp  24434  ghmcnp  24443  eltsms  24461  tsmsf1o  24473  fmucnd  24619  ucnextcn  24631  metcnp3  24868  mbfdm  25956  ismbf  25958  mbfima  25960  ismbfd  25969  mbfimaopnlem  25985  mbfimaopn2  25987  i1fd  26011  ellimc2  26206  limcflf  26210  xrlimcnp  27305  oldval  28229  ubthlem1  31481  disjpreima  33229  imadifxp  33246  preimane  33314  fnpreimac  33315  lmicqusker  34019  ricqusker  34027  algextdeglem4  34402  algextdeg  34407  qtophaus  34518  rhmpreimacnlem  34566  rrhre  34703  mbfmcnvima  34938  imambfm  34944  eulerpartgbij  35054  erdszelem1  36046  erdsze  36057  erdsze2lem2  36059  cvmscbv  36113  cvmsi  36120  cvmsval  36121  cvmliftlem15  36153  opelco3  36635  brimageg  36785  fnimage  36787  imageval  36788  fvimage  36789  filnetlem4  37265  bj-imdirval3  38214  bj-imdirco  38220  ptrest  38646  ismtyhmeolem  38847  ismtybndlem  38849  heibor1lem  38852  zndvdchrrhm  43132  aks6d1c7lem2  43340  aks5lem4a  43349  lmhmfgima  44195  brtrclfv2  44836  csbfv12gALTVD  45989  icccncfext  47005  sge0f1o  47500  smfresal  47906  smfpimbor1lem1  47916  smfpimbor1lem2  47917  smfco  47920  f1cof1b  48255  fnfocofob  48257  imaelsetpreimafv  48585  fundcmpsurinjlem3  48590  imasetpreimafvbijlemfo  48595  fundcmpsurbijinjpreimafv  48597  grimco  49095  uhgrimedgi  49096  isuspgrim0  49100  isuspgrimlem  49101  upgrimwlklem5  49107  gricushgr  49123  grimedg  49141  grtrimap  49154  isubgr3stgrlem5  49176  isubgr3stgrlem6  49177  isubgr3stgrlem7  49178  isubgr3stgrlem8  49179  uspgrlimlem4  49197  grlimedgclnbgr  49201  grlimgrtrilem2  49208