Theorem imaeq2 6027

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5639   ↾ cres 5640   “ cima 5641

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  imaeq2i  6029  imaeq2d  6031  relimasn  6056  cnvimassrndm  6125  funimaexgOLD  6604  fimadmfo  6781  ssimaex  6946  ssimaexg  6947  isoselem  7316  isowe2  7325  f1opw2  7644  mptcnfimad  7965  fnse  8112  supp0cosupp0  8187  tz7.49  8413  ecexr  8676  fopwdom  9049  sbthlem2  9052  sbth  9061  ssenen  9115  sbthfi  9163  fodomfi  9261  imafiOLD  9265  domunfican  9272  fodomfiOLD  9281  f1opwfi  9307  fipreima  9309  marypha1lem  9384  ordtypelem2  9472  ordtypelem3  9473  ordtypelem9  9479  dfac12lem2  10098  dfac12r  10100  ackbij2lem2  10192  ackbij2lem3  10193  r1om  10196  enfin2i  10274  zorn2lem6  10454  zorn2lem7  10455  isacs5lem  18504  acsdrscl  18505  gicsubgen  19211  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmquskerco  19216  gicqusker  19220  efgrelexlema  19679  tgcn  23139  subbascn  23141  iscnp4  23150  cnpnei  23151  cnima  23152  iscncl  23156  cncls  23161  cnconst2  23170  cnrest2  23173  cnprest  23176  cnindis  23179  cncmp  23279  cmpfi  23295  2ndcomap  23345  ptbasfi  23468  xkoopn  23476  xkoccn  23506  txcnp  23507  ptcnplem  23508  txcnmpt  23511  ptrescn  23526  xkoco1cn  23544  xkoco2cn  23545  xkococn  23547  xkoinjcn  23574  elqtop  23584  qtopomap  23605  qtopcmap  23606  ordthmeolem  23688  fbasrn  23771  elfm  23834  elfm2  23835  elfm3  23837  imaelfm  23838  rnelfmlem  23839  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem3  23843  fmfnfmlem4  23844  fmco  23848  flffbas  23882  lmflf  23892  fcfneii  23924  ptcmplem3  23941  ptcmplem5  23943  ptcmpg  23944  cnextcn  23954  symgtgp  23993  ghmcnp  24002  eltsms  24020  tsmsf1o  24032  fmucnd  24179  ucnextcn  24191  metcnp3  24428  mbfdm  25527  ismbf  25529  mbfima  25531  ismbfd  25540  mbfimaopnlem  25556  mbfimaopn2  25558  i1fd  25582  ellimc2  25778  limcflf  25782  xrlimcnp  26878  oldval  27762  ubthlem1  30799  disjpreima  32513  imadifxp  32530  preimane  32594  fnpreimac  32595  lmicqusker  33389  ricqusker  33398  algextdeglem4  33710  algextdeg  33715  qtophaus  33826  rhmpreimacnlem  33874  rrhre  34011  mbfmcnvima  34246  imambfm  34253  eulerpartgbij  34363  erdszelem1  35178  erdsze  35189  erdsze2lem2  35191  cvmscbv  35245  cvmsi  35252  cvmsval  35253  cvmliftlem15  35285  opelco3  35762  brimageg  35915  fnimage  35917  imageval  35918  fvimage  35919  filnetlem4  36369  bj-imdirval3  37172  bj-imdirco  37178  ptrest  37613  ismtyhmeolem  37798  ismtybndlem  37800  heibor1lem  37803  zndvdchrrhm  41960  aks6d1c7lem2  42169  aks5lem4a  42178  lmhmfgima  43073  brtrclfv2  43716  csbfv12gALTVD  44888  icccncfext  45885  sge0f1o  46380  smfresal  46786  smfpimbor1lem1  46796  smfpimbor1lem2  46797  smfco  46800  f1cof1b  47078  fnfocofob  47080  imaelsetpreimafv  47396  fundcmpsurinjlem3  47401  imasetpreimafvbijlemfo  47406  fundcmpsurbijinjpreimafv  47408  grimco  47889  uhgrimedgi  47890  isuspgrim0  47894  isuspgrimlem  47895  upgrimwlklem5  47901  gricushgr  47917  grimedg  47935  grtrimap  47947  isubgr3stgrlem5  47969  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  isubgr3stgrlem8  47972  uspgrlimlem4  47990  grlimgrtrilem2  47994