Theorem imaeq2 5320

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 5255	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5217	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4999	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4999	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2507	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1381   ran crn 4987   |` cres 4988   "cima 4989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435  df-opab 4493  df-xp 4992  df-cnv 4994  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999

This theorem is referenced by:  imaeq2i  5322  imaeq2d  5324  relimasn  5347  funimaexg  5652  ssimaex  5920  ssimaexg  5921  isoselem  6219  isowe2  6228  f1opw2  6510  fnse  6899  supp0cosupp0  6938  tz7.49  7109  ecexr  7315  fopwdom  7624  sbthlem2  7627  sbth  7636  ssenen  7690  domunfican  7792  fodomfi  7798  f1opwfi  7823  fipreima  7825  marypha1lem  7892  ordtypelem2  7944  ordtypelem3  7945  ordtypelem9  7951  dfac12lem2  8524  dfac12r  8526  ackbij2lem2  8620  ackbij2lem3  8621  r1om  8624  enfin2i  8701  zorn2lem6  8881  zorn2lem7  8882  isacs5lem  15670  acsdrscl  15671  gicsubgen  16197  efgrelexlema  16638  gsumval3OLD  16779  tgcn  19623  subbascn  19625  iscnp4  19634  cnpnei  19635  cnima  19636  iscncl  19640  cncls  19645  cnconst2  19654  cnrest2  19657  cnprest  19660  cnindis  19663  cncmp  19762  cmpfi  19778  2ndcomap  19829  ptbasfi  19952  xkoopn  19960  xkoccn  19990  txcnp  19991  ptcnplem  19992  txcnmpt  19995  ptrescn  20010  xkoco1cn  20028  xkoco2cn  20029  xkococn  20031  xkoinjcn  20058  elqtop  20068  qtopomap  20089  qtopcmap  20090  ordthmeolem  20172  fbasrn  20255  elfm  20318  elfm2  20319  elfm3  20321  imaelfm  20322  rnelfmlem  20323  rnelfm  20324  fmfnfmlem2  20326  fmfnfmlem3  20327  fmfnfmlem4  20328  fmco  20332  flffbas  20366  lmflf  20376  fcfneii  20408  ptcmplem3  20424  ptcmplem5  20426  ptcmpg  20427  cnextcn  20437  symgtgp  20470  ghmcnp  20483  eltsms  20501  tsmsf1o  20517  fmucnd  20665  ucnextcn  20677  metcnp3  20913  mbfdm  21905  ismbf  21907  mbfima  21909  ismbfd  21917  mbfimaopnlem  21932  mbfimaopn2  21934  i1fd  21958  ellimc2  22151  limcflf  22155  xrlimcnp  23167  ubthlem1  25655  disjpreima  27314  imadifxp  27327  qtophaus  27709  rrhre  27869  mbfmcnvima  28098  imambfm  28103  eulerpartgbij  28181  erdszelem1  28505  erdsze  28516  erdsze2lem2  28518  cvmscbv  28573  cvmsi  28580  cvmsval  28581  cvmliftlem15  28613  opelco3  29180  brimageg  29549  fnimage  29551  imageval  29552  fvimage  29553  ptrest  30020  filnetlem4  30171  ismtyhmeolem  30272  ismtybndlem  30274  heibor1lem  30277  lmhmfgima  31002  icccncfext  31597  csbfv12gALTVD  33427