Theorem imaeq2 5331

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 5266	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5228	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 5012	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 5012	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2533	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1379   ran crn 5000   |` cres 5001   "cima 5002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012

This theorem is referenced by:  imaeq2i  5333  imaeq2d  5335  relimasn  5358  funimaexg  5663  ssimaex  5930  ssimaexg  5931  isoselem  6223  isowe2  6232  f1opw2  6510  fnse  6897  supp0cosupp0  6936  tz7.49  7107  ecexr  7313  fopwdom  7622  sbthlem2  7625  sbth  7634  ssenen  7688  domunfican  7789  fodomfi  7795  f1opwfi  7820  fipreima  7822  marypha1lem  7889  ordtypelem2  7940  ordtypelem3  7941  ordtypelem9  7947  dfac12lem2  8520  dfac12r  8522  ackbij2lem2  8616  ackbij2lem3  8617  r1om  8620  enfin2i  8697  zorn2lem6  8877  zorn2lem7  8878  isacs5lem  15652  acsdrscl  15653  gicsubgen  16121  efgrelexlema  16563  gsumval3OLD  16699  tgcn  19519  subbascn  19521  iscnp4  19530  cnpnei  19531  cnima  19532  iscncl  19536  cncls  19541  cnconst2  19550  cnrest2  19553  cnprest  19556  cnindis  19559  cncmp  19658  cmpfi  19674  2ndcomap  19725  ptbasfi  19817  xkoopn  19825  xkoccn  19855  txcnp  19856  ptcnplem  19857  txcnmpt  19860  ptrescn  19875  xkoco1cn  19893  xkoco2cn  19894  xkococn  19896  xkoinjcn  19923  elqtop  19933  qtopomap  19954  qtopcmap  19955  ordthmeolem  20037  fbasrn  20120  elfm  20183  elfm2  20184  elfm3  20186  imaelfm  20187  rnelfmlem  20188  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem3  20192  fmfnfmlem4  20193  fmco  20197  flffbas  20231  lmflf  20241  fcfneii  20273  ptcmplem3  20289  ptcmplem5  20291  ptcmpg  20292  cnextcn  20302  symgtgp  20335  ghmcnp  20348  eltsms  20366  tsmsf1o  20382  fmucnd  20530  ucnextcn  20542  metcnp3  20778  mbfdm  21770  ismbf  21772  mbfima  21774  ismbfd  21782  mbfimaopnlem  21797  mbfimaopn2  21799  i1fd  21823  ellimc2  22016  limcflf  22020  xrlimcnp  23026  ubthlem1  25462  disjpreima  27118  imadifxp  27131  rrhre  27635  qtophaus  27637  mbfmcnvima  27868  imambfm  27873  eulerpartgbij  27951  erdszelem1  28275  erdsze  28286  erdsze2lem2  28288  cvmscbv  28343  cvmsi  28350  cvmsval  28351  cvmliftlem15  28383  opelco3  28785  brimageg  29154  fnimage  29156  imageval  29157  fvimage  29158  ptrest  29625  filnetlem4  29802  ismtyhmeolem  29903  ismtybndlem  29905  heibor1lem  29908  lmhmfgima  30634  icccncfext  31226  csbfv12gALTVD  32779