Theorem imaeq2 5183

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 5119	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5081	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4866	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4866	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2488	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1437   ran crn 4854   |` cres 4855   "cima 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866

This theorem is referenced by:  imaeq2i  5185  imaeq2d  5187  relimasn  5210  funimaexg  5678  ssimaex  5946  ssimaexg  5947  isoselem  6247  isowe2  6256  f1opw2  6536  fnse  6924  supp0cosupp0  6965  tz7.49  7173  ecexr  7379  fopwdom  7689  sbthlem2  7692  sbth  7701  ssenen  7755  domunfican  7853  fodomfi  7859  f1opwfi  7887  fipreima  7889  marypha1lem  7956  ordtypelem2  8043  ordtypelem3  8044  ordtypelem9  8050  dfac12lem2  8581  dfac12r  8583  ackbij2lem2  8677  ackbij2lem3  8678  r1om  8681  enfin2i  8758  zorn2lem6  8938  zorn2lem7  8939  isacs5lem  16414  acsdrscl  16415  gicsubgen  16941  efgrelexlema  17398  tgcn  20266  subbascn  20268  iscnp4  20277  cnpnei  20278  cnima  20279  iscncl  20283  cncls  20288  cnconst2  20297  cnrest2  20300  cnprest  20303  cnindis  20306  cncmp  20405  cmpfi  20421  2ndcomap  20471  ptbasfi  20594  xkoopn  20602  xkoccn  20632  txcnp  20633  ptcnplem  20634  txcnmpt  20637  ptrescn  20652  xkoco1cn  20670  xkoco2cn  20671  xkococn  20673  xkoinjcn  20700  elqtop  20710  qtopomap  20731  qtopcmap  20732  ordthmeolem  20814  fbasrn  20897  elfm  20960  elfm2  20961  elfm3  20963  imaelfm  20964  rnelfmlem  20965  rnelfm  20966  fmfnfmlem2  20968  fmfnfmlem3  20969  fmfnfmlem4  20970  fmco  20974  flffbas  21008  lmflf  21018  fcfneii  21050  ptcmplem3  21067  ptcmplem5  21069  ptcmpg  21070  cnextcn  21080  symgtgp  21114  ghmcnp  21127  eltsms  21145  tsmsf1o  21157  fmucnd  21305  ucnextcn  21317  metcnp3  21553  mbfdm  22582  ismbf  22584  mbfima  22586  ismbfd  22594  mbfimaopnlem  22609  mbfimaopn2  22611  i1fd  22637  ellimc2  22830  limcflf  22834  xrlimcnp  23892  ubthlem1  26510  disjpreima  28196  imadifxp  28214  qtophaus  28671  rrhre  28833  mbfmcnvima  29087  imambfm  29092  eulerpartgbij  29213  erdszelem1  29922  erdsze  29933  erdsze2lem2  29935  cvmscbv  29989  cvmsi  29996  cvmsval  29997  cvmliftlem15  30029  opelco3  30427  brimageg  30699  fnimage  30701  imageval  30702  fvimage  30703  filnetlem4  31042  ptrest  31903  ismtyhmeolem  32100  ismtybndlem  32102  heibor1lem  32105  lmhmfgima  35912  brtrclfv2  36289  csbfv12gALTVD  37269  icccncfext  37705  sge0f1o  38132