Theorem imaeq2 5153

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 5092	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5054	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4840	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4840	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2490	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1362   ran crn 4828   |` cres 4829   "cima 4830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-cnv 4835  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840

This theorem is referenced by:  imaeq2i  5155  imaeq2d  5157  relimasn  5180  funimaexg  5483  ssimaex  5744  ssimaexg  5745  isoselem  6019  isowe2  6028  f1opw2  6302  fnse  6678  supp0cosupp0  6717  tz7.49  6886  ecexr  7094  fopwdom  7407  sbthlem2  7410  sbth  7419  ssenen  7473  domunfican  7572  fodomfi  7578  f1opwfi  7603  fipreima  7605  marypha1lem  7671  ordtypelem2  7721  ordtypelem3  7722  ordtypelem9  7728  dfac12lem2  8301  dfac12r  8303  ackbij2lem2  8397  ackbij2lem3  8398  r1om  8401  enfin2i  8478  zorn2lem6  8658  zorn2lem7  8659  isacs5lem  15321  acsdrscl  15322  gicsubgen  15785  efgrelexlema  16225  gsumval3OLD  16361  tgcn  18697  subbascn  18699  iscnp4  18708  cnpnei  18709  cnima  18710  iscncl  18714  cncls  18719  cnconst2  18728  cnrest2  18731  cnprest  18734  cnindis  18737  cncmp  18836  cmpfi  18852  2ndcomap  18903  ptbasfi  18995  xkoopn  19003  xkoccn  19033  txcnp  19034  ptcnplem  19035  txcnmpt  19038  ptrescn  19053  xkoco1cn  19071  xkoco2cn  19072  xkococn  19074  xkoinjcn  19101  elqtop  19111  qtopomap  19132  qtopcmap  19133  ordthmeolem  19215  fbasrn  19298  elfm  19361  elfm2  19362  elfm3  19364  imaelfm  19365  rnelfmlem  19366  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem3  19370  fmfnfmlem4  19371  fmco  19375  flffbas  19409  lmflf  19419  fcfneii  19451  ptcmplem3  19467  ptcmplem5  19469  ptcmpg  19470  cnextcn  19480  symgtgp  19513  ghmcnp  19526  eltsms  19544  tsmsf1o  19560  fmucnd  19708  ucnextcn  19720  metcnp3  19956  mbfdm  20947  ismbf  20949  mbfima  20951  ismbfd  20959  mbfimaopnlem  20974  mbfimaopn2  20976  i1fd  21000  ellimc2  21193  limcflf  21197  xrlimcnp  22246  ubthlem1  24093  disjpreima  25751  imadifxp  25762  rrhre  26300  mbfmcnvima  26525  imambfm  26530  eulerpartgbij  26602  erdszelem1  26926  erdsze  26937  erdsze2lem2  26939  cvmscbv  26994  cvmsi  27001  cvmsval  27002  cvmliftlem15  27034  opelco3  27435  brimageg  27804  fnimage  27806  imageval  27807  fvimage  27808  ptrest  28266  filnetlem4  28443  ismtyhmeolem  28544  ismtybndlem  28546  heibor1lem  28549  lmhmfgima  29279  csbfv12gALTVD  31334