Theorem imaeq2 6016

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 5934	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5891	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5644	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5644	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5632   ↾ cres 5633   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq2i  6018  imaeq2d  6020  relimasn  6045  cnvimassrndm  6113  fimadmfo  6763  ssimaex  6928  ssimaexg  6929  isoselem  7298  isowe2  7307  f1opw2  7624  mptcnfimad  7944  fnse  8089  supp0cosupp0  8164  tz7.49  8390  ecexr  8653  fopwdom  9026  sbthlem2  9029  sbth  9038  ssenen  9092  sbthfi  9140  fodomfi  9237  imafiOLD  9241  domunfican  9248  fodomfiOLD  9257  f1opwfi  9283  fipreima  9285  marypha1lem  9360  ordtypelem2  9448  ordtypelem3  9449  ordtypelem9  9455  dfac12lem2  10074  dfac12r  10076  ackbij2lem2  10168  ackbij2lem3  10169  r1om  10172  enfin2i  10250  zorn2lem6  10430  zorn2lem7  10431  isacs5lem  18480  acsdrscl  18481  gicsubgen  19187  ghmqusnsglem1  19188  ghmquskerlem1  19191  ghmquskerco  19192  gicqusker  19196  efgrelexlema  19655  tgcn  23115  subbascn  23117  iscnp4  23126  cnpnei  23127  cnima  23128  iscncl  23132  cncls  23137  cnconst2  23146  cnrest2  23149  cnprest  23152  cnindis  23155  cncmp  23255  cmpfi  23271  2ndcomap  23321  ptbasfi  23444  xkoopn  23452  xkoccn  23482  txcnp  23483  ptcnplem  23484  txcnmpt  23487  ptrescn  23502  xkoco1cn  23520  xkoco2cn  23521  xkococn  23523  xkoinjcn  23550  elqtop  23560  qtopomap  23581  qtopcmap  23582  ordthmeolem  23664  fbasrn  23747  elfm  23810  elfm2  23811  elfm3  23813  imaelfm  23814  rnelfmlem  23815  rnelfm  23816  fmfnfmlem2  23818  fmfnfmlem3  23819  fmfnfmlem4  23820  fmco  23824  flffbas  23858  lmflf  23868  fcfneii  23900  ptcmplem3  23917  ptcmplem5  23919  ptcmpg  23920  cnextcn  23930  symgtgp  23969  ghmcnp  23978  eltsms  23996  tsmsf1o  24008  fmucnd  24155  ucnextcn  24167  metcnp3  24404  mbfdm  25503  ismbf  25505  mbfima  25507  ismbfd  25516  mbfimaopnlem  25532  mbfimaopn2  25534  i1fd  25558  ellimc2  25754  limcflf  25758  xrlimcnp  26854  oldval  27738  ubthlem1  30772  disjpreima  32486  imadifxp  32503  preimane  32567  fnpreimac  32568  lmicqusker  33362  ricqusker  33371  algextdeglem4  33683  algextdeg  33688  qtophaus  33799  rhmpreimacnlem  33847  rrhre  33984  mbfmcnvima  34219  imambfm  34226  eulerpartgbij  34336  erdszelem1  35151  erdsze  35162  erdsze2lem2  35164  cvmscbv  35218  cvmsi  35225  cvmsval  35226  cvmliftlem15  35258  opelco3  35735  brimageg  35888  fnimage  35890  imageval  35891  fvimage  35892  filnetlem4  36342  bj-imdirval3  37145  bj-imdirco  37151  ptrest  37586  ismtyhmeolem  37771  ismtybndlem  37773  heibor1lem  37776  zndvdchrrhm  41933  aks6d1c7lem2  42142  aks5lem4a  42151  lmhmfgima  43046  brtrclfv2  43689  csbfv12gALTVD  44861  icccncfext  45858  sge0f1o  46353  smfresal  46759  smfpimbor1lem1  46769  smfpimbor1lem2  46770  smfco  46773  f1cof1b  47051  fnfocofob  47053  imaelsetpreimafv  47369  fundcmpsurinjlem3  47374  imasetpreimafvbijlemfo  47379  fundcmpsurbijinjpreimafv  47381  grimco  47862  uhgrimedgi  47863  isuspgrim0  47867  isuspgrimlem  47868  upgrimwlklem5  47874  gricushgr  47890  grimedg  47908  grtrimap  47920  isubgr3stgrlem5  47942  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  isubgr3stgrlem8  47945  uspgrlimlem4  47963  grlimgrtrilem2  47967