Theorem imaeq2 5158

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq2	|- ( A = B -> ( C " A ) = ( C " B ) )

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 5100	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5056	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4850	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4850	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2461	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1649   ran crn 4838   |` cres 4839   "cima 4840

This theorem is referenced by:  imaeq2i  5160  imaeq2d  5162  relimasn  5186  funimaexg  5489  ssimaex  5747  ssimaexg  5748  isoselem  6020  isowe2  6029  f1opw2  6257  fnse  6422  tz7.49  6661  ecexr  6869  fopwdom  7175  sbthlem2  7177  sbth  7186  ssenen  7240  domunfican  7338  fodomfi  7344  f1opwfi  7368  fipreima  7370  marypha1lem  7396  ordtypelem2  7444  ordtypelem3  7445  ordtypelem9  7451  dfac12lem2  7980  dfac12r  7982  ackbij2lem2  8076  ackbij2lem3  8077  r1om  8080  enfin2i  8157  zorn2lem6  8337  zorn2lem7  8338  isacs5lem  14550  acsdrscl  14551  gicsubgen  15020  efgrelexlema  15336  gsumval3  15469  tgcn  17270  subbascn  17272  iscnp4  17281  cnpnei  17282  cnima  17283  iscncl  17287  cncls  17292  cnconst2  17301  cnrest2  17304  cnprest  17307  cnindis  17310  cncmp  17409  cmpfi  17425  2ndcomap  17474  ptbasfi  17566  xkoopn  17574  xkoccn  17604  txcnp  17605  ptcnplem  17606  txcnmpt  17609  ptrescn  17624  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  elqtop  17682  qtopomap  17703  qtopcmap  17704  ordthmeolem  17786  fbasrn  17869  elfm  17932  elfm2  17933  elfm3  17935  imaelfm  17936  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem3  17941  fmfnfmlem4  17942  fmco  17946  flffbas  17980  lmflf  17990  fcfneii  18022  ptcmplem3  18038  ptcmplem5  18040  ptcmpg  18041  cnextcn  18051  symgtgp  18084  ghmcnp  18097  eltsms  18115  tsmsf1o  18127  fmucnd  18275  ucnextcn  18287  metcnp3  18523  mbfdm  19473  ismbf  19475  mbfima  19477  ismbfd  19485  mbfimaopnlem  19500  mbfimaopn2  19502  i1fd  19526  ellimc2  19717  limcflf  19721  xrlimcnp  20760  ubthlem1  22325  disjpreima  23979  imadifxp  23991  rrhre  24340  mbfmcnvima  24560  imambfm  24565  erdszelem1  24830  erdsze  24841  erdsze2lem2  24843  cvmscbv  24898  cvmsi  24905  cvmsval  24906  cvmliftlem15  24938  brimageg  25680  fnimage  25682  imageval  25683  fvimage  25684  filnetlem4  26300  ismtyhmeolem  26403  ismtybndlem  26405  heibor1lem  26408  lmhmfgima  27050  csbfv12gALTVD  28720

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850