Theorem imaeq2 5272

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 5212	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5174	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4960	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4960	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2520	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1370   ran crn 4948   |` cres 4949   "cima 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-xp 4953  df-cnv 4955  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960

This theorem is referenced by:  imaeq2i  5274  imaeq2d  5276  relimasn  5299  funimaexg  5602  ssimaex  5864  ssimaexg  5865  isoselem  6140  isowe2  6149  f1opw2  6422  fnse  6798  supp0cosupp0  6837  tz7.49  7009  ecexr  7215  fopwdom  7528  sbthlem2  7531  sbth  7540  ssenen  7594  domunfican  7694  fodomfi  7700  f1opwfi  7725  fipreima  7727  marypha1lem  7793  ordtypelem2  7843  ordtypelem3  7844  ordtypelem9  7850  dfac12lem2  8423  dfac12r  8425  ackbij2lem2  8519  ackbij2lem3  8520  r1om  8523  enfin2i  8600  zorn2lem6  8780  zorn2lem7  8781  isacs5lem  15457  acsdrscl  15458  gicsubgen  15924  efgrelexlema  16366  gsumval3OLD  16502  tgcn  18987  subbascn  18989  iscnp4  18998  cnpnei  18999  cnima  19000  iscncl  19004  cncls  19009  cnconst2  19018  cnrest2  19021  cnprest  19024  cnindis  19027  cncmp  19126  cmpfi  19142  2ndcomap  19193  ptbasfi  19285  xkoopn  19293  xkoccn  19323  txcnp  19324  ptcnplem  19325  txcnmpt  19328  ptrescn  19343  xkoco1cn  19361  xkoco2cn  19362  xkococn  19364  xkoinjcn  19391  elqtop  19401  qtopomap  19422  qtopcmap  19423  ordthmeolem  19505  fbasrn  19588  elfm  19651  elfm2  19652  elfm3  19654  imaelfm  19655  rnelfmlem  19656  rnelfm  19657  fmfnfmlem2  19659  fmfnfmlem3  19660  fmfnfmlem4  19661  fmco  19665  flffbas  19699  lmflf  19709  fcfneii  19741  ptcmplem3  19757  ptcmplem5  19759  ptcmpg  19760  cnextcn  19770  symgtgp  19803  ghmcnp  19816  eltsms  19834  tsmsf1o  19850  fmucnd  19998  ucnextcn  20010  metcnp3  20246  mbfdm  21238  ismbf  21240  mbfima  21242  ismbfd  21250  mbfimaopnlem  21265  mbfimaopn2  21267  i1fd  21291  ellimc2  21484  limcflf  21488  xrlimcnp  22494  ubthlem1  24422  disjpreima  26078  imadifxp  26089  rrhre  26591  mbfmcnvima  26815  imambfm  26820  eulerpartgbij  26898  erdszelem1  27222  erdsze  27233  erdsze2lem2  27235  cvmscbv  27290  cvmsi  27297  cvmsval  27298  cvmliftlem15  27330  opelco3  27732  brimageg  28101  fnimage  28103  imageval  28104  fvimage  28105  ptrest  28572  filnetlem4  28749  ismtyhmeolem  28850  ismtybndlem  28852  heibor1lem  28855  lmhmfgima  29584  csbfv12gALTVD  31952