Theorem imaeq2 6052

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5656   ↾ cres 5657   “ cima 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  imaeq2i  6054  imaeq2d  6056  relimasn  6081  cnvimassrndm  6143  fimadmfo  6798  ssimaex  6963  ssimaexg  6964  isoselem  7342  isowe2  7351  f1opw2  7669  mptcnfimad  7983  fnse  8131  supp0cosupp0  8206  tz7.49  8434  ecexr  8701  fopwdom  9083  sbthlem2  9086  sbth  9095  ssenen  9149  sbthfi  9193  fodomfi  9282  domunfican  9291  f1opwfi  9323  fipreima  9325  marypha1lem  9403  ordtypelem2  9491  ordtypelem3  9492  ordtypelem9  9498  dfac12lem2  10147  dfac12r  10149  ackbij2lem2  10241  ackbij2lem3  10242  r1om  10245  enfin2i  10323  zorn2lem6  10503  zorn2lem7  10504  isacs5lem  18633  acsdrscl  18634  gicsubgen  19406  ghmqusnsglem1  19407  ghmquskerlem1  19410  ghmquskerco  19411  gicqusker  19415  efgrelexlema  19876  tgcn  23477  subbascn  23479  iscnp4  23488  cnpnei  23489  cnima  23490  iscncl  23494  cncls  23499  cnconst2  23508  cnrest2  23511  cnprest  23514  cnindis  23517  cncmp  23617  cmpfi  23633  2ndcomap  23684  ptbasfi  23807  xkoopn  23815  xkoccn  23845  txcnp  23846  ptcnplem  23847  txcnmpt  23850  ptrescn  23865  xkoco1cn  23883  xkoco2cn  23884  xkococn  23886  xkoinjcn  23913  elqtop  23923  qtopomap  23944  qtopcmap  23945  ordthmeolem  24027  fbasrn  24110  elfm  24173  elfm2  24174  elfm3  24176  imaelfm  24177  rnelfmlem  24178  rnelfm  24179  fmfnfmlem2  24181  fmfnfmlem3  24182  fmfnfmlem4  24183  fmco  24187  flffbas  24221  lmflf  24231  fcfneii  24263  ptcmplem3  24280  ptcmplem5  24282  ptcmpg  24283  cnextcn  24293  symgtgp  24332  ghmcnp  24341  eltsms  24359  tsmsf1o  24371  fmucnd  24517  ucnextcn  24529  metcnp3  24766  mbfdm  25854  ismbf  25856  mbfima  25858  ismbfd  25867  mbfimaopnlem  25883  mbfimaopn2  25885  i1fd  25909  ellimc2  26104  limcflf  26108  xrlimcnp  27205  oldval  28099  ubthlem1  31351  disjpreima  33057  imadifxp  33074  preimane  33142  fnpreimac  33143  lmicqusker  33847  ricqusker  33855  algextdeglem4  34230  algextdeg  34235  qtophaus  34346  rhmpreimacnlem  34394  rrhre  34531  mbfmcnvima  34766  imambfm  34773  eulerpartgbij  34883  erdszelem1  35770  erdsze  35781  erdsze2lem2  35783  cvmscbv  35837  cvmsi  35844  cvmsval  35845  cvmliftlem15  35877  opelco3  36354  brimageg  36504  fnimage  36506  imageval  36507  fvimage  36508  filnetlem4  37000  bj-imdirval3  37936  bj-imdirco  37942  ptrest  38368  ismtyhmeolem  38554  ismtybndlem  38556  heibor1lem  38559  zndvdchrrhm  42839  aks6d1c7lem2  43047  aks5lem4a  43056  lmhmfgima  43925  brtrclfv2  44567  csbfv12gALTVD  45721  icccncfext  46715  sge0f1o  47210  smfresal  47616  smfpimbor1lem1  47626  smfpimbor1lem2  47627  smfco  47630  f1cof1b  47965  fnfocofob  47967  imaelsetpreimafv  48295  fundcmpsurinjlem3  48300  imasetpreimafvbijlemfo  48305  fundcmpsurbijinjpreimafv  48307  grimco  48805  uhgrimedgi  48806  isuspgrim0  48810  isuspgrimlem  48811  upgrimwlklem5  48817  gricushgr  48833  grimedg  48851  grtrimap  48864  isubgr3stgrlem5  48886  isubgr3stgrlem6  48887  isubgr3stgrlem7  48888  isubgr3stgrlem8  48889  uspgrlimlem4  48907  grlimedgclnbgr  48911  grlimgrtrilem2  48918