Theorem imaeq2 5703

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 5624	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5585	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5355	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5355	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2886	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1658  ran crn 5343   ↾ cres 5344   “ cima 5345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-opab 4936  df-xp 5348  df-cnv 5350  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355

This theorem is referenced by:  imaeq2i  5705  imaeq2d  5707  relimasn  5729  funimaexg  6208  fimadmfo  6362  ssimaex  6510  ssimaexg  6511  isoselem  6846  isowe2  6855  f1opw2  7148  fnse  7558  supp0cosupp0  7599  tz7.49  7806  ecexr  8014  fopwdom  8337  sbthlem2  8340  sbth  8349  ssenen  8403  domunfican  8502  fodomfi  8508  f1opwfi  8539  fipreima  8541  marypha1lem  8608  ordtypelem2  8693  ordtypelem3  8694  ordtypelem9  8700  dfac12lem2  9281  dfac12r  9283  ackbij2lem2  9377  ackbij2lem3  9378  r1om  9381  enfin2i  9458  zorn2lem6  9638  zorn2lem7  9639  isacs5lem  17522  acsdrscl  17523  gicsubgen  18071  efgrelexlema  18515  tgcn  21427  subbascn  21429  iscnp4  21438  cnpnei  21439  cnima  21440  iscncl  21444  cncls  21449  cnconst2  21458  cnrest2  21461  cnprest  21464  cnindis  21467  cncmp  21566  cmpfi  21582  2ndcomap  21632  ptbasfi  21755  xkoopn  21763  xkoccn  21793  txcnp  21794  ptcnplem  21795  txcnmpt  21798  ptrescn  21813  xkoco1cn  21831  xkoco2cn  21832  xkococn  21834  xkoinjcn  21861  elqtop  21871  qtopomap  21892  qtopcmap  21893  ordthmeolem  21975  fbasrn  22058  elfm  22121  elfm2  22122  elfm3  22124  imaelfm  22125  rnelfmlem  22126  rnelfm  22127  fmfnfmlem2  22129  fmfnfmlem3  22130  fmfnfmlem4  22131  fmco  22135  flffbas  22169  lmflf  22179  fcfneii  22211  ptcmplem3  22228  ptcmplem5  22230  ptcmpg  22231  cnextcn  22241  symgtgp  22275  ghmcnp  22288  eltsms  22306  tsmsf1o  22318  fmucnd  22466  ucnextcn  22478  metcnp3  22715  mbfdm  23792  ismbf  23794  mbfima  23796  ismbfd  23805  mbfimaopnlem  23821  mbfimaopn2  23823  i1fd  23847  ellimc2  24040  limcflf  24044  xrlimcnp  25108  ubthlem1  28281  disjpreima  29944  imadifxp  29961  qtophaus  30448  rrhre  30610  mbfmcnvima  30864  imambfm  30869  eulerpartgbij  30979  erdszelem1  31719  erdsze  31730  erdsze2lem2  31732  cvmscbv  31786  cvmsi  31793  cvmsval  31794  cvmliftlem15  31826  opelco3  32216  brimageg  32573  fnimage  32575  imageval  32576  fvimage  32577  filnetlem4  32914  ptrest  33952  ismtyhmeolem  34145  ismtybndlem  34147  heibor1lem  34150  lmhmfgima  38497  brtrclfv2  38860  csbfv12gALTVD  39953  icccncfext  40895  sge0f1o  41390  smfresal  41789  smfpimbor1lem1  41799  smfpimbor1lem2  41800  smfco  41803  isomushgr  42544  isomuspgrlem1  42545  isomuspgrlem2a  42546  isomuspgrlem2b  42547  isomuspgrlem2c  42548  isomuspgrlem2d  42549  isomuspgr  42552  isomgrsym  42554