Theorem imaeq2 5160

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 5062	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4848	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4848	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1369   ran crn 4836   |` cres 4837   "cima 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-xp 4841  df-cnv 4843  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848

This theorem is referenced by:  imaeq2i  5162  imaeq2d  5164  relimasn  5187  funimaexg  5490  ssimaex  5751  ssimaexg  5752  isoselem  6027  isowe2  6036  f1opw2  6308  fnse  6684  supp0cosupp0  6723  tz7.49  6892  ecexr  7098  fopwdom  7411  sbthlem2  7414  sbth  7423  ssenen  7477  domunfican  7576  fodomfi  7582  f1opwfi  7607  fipreima  7609  marypha1lem  7675  ordtypelem2  7725  ordtypelem3  7726  ordtypelem9  7732  dfac12lem2  8305  dfac12r  8307  ackbij2lem2  8401  ackbij2lem3  8402  r1om  8405  enfin2i  8482  zorn2lem6  8662  zorn2lem7  8663  isacs5lem  15331  acsdrscl  15332  gicsubgen  15797  efgrelexlema  16237  gsumval3OLD  16373  tgcn  18836  subbascn  18838  iscnp4  18847  cnpnei  18848  cnima  18849  iscncl  18853  cncls  18858  cnconst2  18867  cnrest2  18870  cnprest  18873  cnindis  18876  cncmp  18975  cmpfi  18991  2ndcomap  19042  ptbasfi  19134  xkoopn  19142  xkoccn  19172  txcnp  19173  ptcnplem  19174  txcnmpt  19177  ptrescn  19192  xkoco1cn  19210  xkoco2cn  19211  xkococn  19213  xkoinjcn  19240  elqtop  19250  qtopomap  19271  qtopcmap  19272  ordthmeolem  19354  fbasrn  19437  elfm  19500  elfm2  19501  elfm3  19503  imaelfm  19504  rnelfmlem  19505  rnelfm  19506  fmfnfmlem2  19508  fmfnfmlem3  19509  fmfnfmlem4  19510  fmco  19514  flffbas  19548  lmflf  19558  fcfneii  19590  ptcmplem3  19606  ptcmplem5  19608  ptcmpg  19609  cnextcn  19619  symgtgp  19652  ghmcnp  19665  eltsms  19683  tsmsf1o  19699  fmucnd  19847  ucnextcn  19859  metcnp3  20095  mbfdm  21086  ismbf  21088  mbfima  21090  ismbfd  21098  mbfimaopnlem  21113  mbfimaopn2  21115  i1fd  21139  ellimc2  21332  limcflf  21336  xrlimcnp  22342  ubthlem1  24243  disjpreima  25900  imadifxp  25911  rrhre  26420  mbfmcnvima  26645  imambfm  26650  eulerpartgbij  26728  erdszelem1  27052  erdsze  27063  erdsze2lem2  27065  cvmscbv  27120  cvmsi  27127  cvmsval  27128  cvmliftlem15  27160  opelco3  27562  brimageg  27931  fnimage  27933  imageval  27934  fvimage  27935  ptrest  28399  filnetlem4  28576  ismtyhmeolem  28677  ismtybndlem  28679  heibor1lem  28682  lmhmfgima  29411  csbfv12gALTVD  31567