Theorem imaeq2 5962

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 5883	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5844	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5601	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5601	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  ran crn 5589   ↾ cres 5590   “ cima 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-xp 5594  df-cnv 5596  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601

This theorem is referenced by:  imaeq2i  5964  imaeq2d  5966  relimasn  5989  cnvimassrndm  6052  funimaexg  6516  fimadmfo  6693  ssimaex  6847  ssimaexg  6848  isoselem  7205  isowe2  7214  f1opw2  7515  fnse  7958  supp0cosupp0  8008  tz7.49  8260  ecexr  8477  fopwdom  8836  sbthlem2  8840  sbth  8849  ssenen  8903  imafi  8923  sbthfi  8950  domunfican  9048  fodomfi  9053  f1opwfi  9084  fipreima  9086  marypha1lem  9153  ordtypelem2  9239  ordtypelem3  9240  ordtypelem9  9246  dfac12lem2  9884  dfac12r  9886  ackbij2lem2  9980  ackbij2lem3  9981  r1om  9984  enfin2i  10061  zorn2lem6  10241  zorn2lem7  10242  isacs5lem  18244  acsdrscl  18245  gicsubgen  18875  efgrelexlema  19336  tgcn  22384  subbascn  22386  iscnp4  22395  cnpnei  22396  cnima  22397  iscncl  22401  cncls  22406  cnconst2  22415  cnrest2  22418  cnprest  22421  cnindis  22424  cncmp  22524  cmpfi  22540  2ndcomap  22590  ptbasfi  22713  xkoopn  22721  xkoccn  22751  txcnp  22752  ptcnplem  22753  txcnmpt  22756  ptrescn  22771  xkoco1cn  22789  xkoco2cn  22790  xkococn  22792  xkoinjcn  22819  elqtop  22829  qtopomap  22850  qtopcmap  22851  ordthmeolem  22933  fbasrn  23016  elfm  23079  elfm2  23080  elfm3  23082  imaelfm  23083  rnelfmlem  23084  rnelfm  23085  fmfnfmlem2  23087  fmfnfmlem3  23088  fmfnfmlem4  23089  fmco  23093  flffbas  23127  lmflf  23137  fcfneii  23169  ptcmplem3  23186  ptcmplem5  23188  ptcmpg  23189  cnextcn  23199  symgtgp  23238  ghmcnp  23247  eltsms  23265  tsmsf1o  23277  fmucnd  23425  ucnextcn  23437  metcnp3  23677  mbfdm  24771  ismbf  24773  mbfima  24775  ismbfd  24784  mbfimaopnlem  24800  mbfimaopn2  24802  i1fd  24826  ellimc2  25022  limcflf  25026  xrlimcnp  26099  ubthlem1  29211  disjpreima  30902  imadifxp  30919  preimane  30986  fnpreimac  30987  qtophaus  31765  rhmpreimacnlem  31813  rrhre  31950  mbfmcnvima  32203  imambfm  32208  eulerpartgbij  32318  erdszelem1  33132  erdsze  33143  erdsze2lem2  33145  cvmscbv  33199  cvmsi  33206  cvmsval  33207  cvmliftlem15  33239  opelco3  33728  oldval  34017  brimageg  34208  fnimage  34210  imageval  34211  fvimage  34212  filnetlem4  34549  bj-imdirval3  35334  bj-imdirco  35340  ptrest  35755  ismtyhmeolem  35941  ismtybndlem  35943  heibor1lem  35946  lmhmfgima  40889  brtrclfv2  41288  csbfv12gALTVD  42472  icccncfext  43382  sge0f1o  43874  smfresal  44273  smfpimbor1lem1  44283  smfpimbor1lem2  44284  smfco  44287  f1cof1b  44520  fnfocofob  44522  imaelsetpreimafv  44799  fundcmpsurinjlem3  44804  imasetpreimafvbijlemfo  44809  fundcmpsurbijinjpreimafv  44811  isomushgr  45230  isomuspgrlem1  45231  isomuspgrlem2a  45232  isomuspgrlem2b  45233  isomuspgrlem2c  45234  isomuspgrlem2d  45235  isomuspgr  45238  isomgrsym  45240