Theorem imaeq2 4260

Description: Equality theorem for image.

Assertion

Ref	Expression
imaeq2	|- (A = B -> (C"A) = (C"B))

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 4219	. . 3 |- (A = B -> (C |` A) = (C |` B))
2	1	rneqd 4188	. 2 |- (A = B -> ran ( C |` A) = ran ( C |` B))
3		df-ima 4007	. 2 |- (C"A) = ran ( C |` A)
4		df-ima 4007	. 2 |- (C"B) = ran ( C |` B)
5	2, 3, 4	3eqtr4g 1953	1 |- (A = B -> (C"A) = (C"B))

Syntax hints:   -> wi 3   = wceq 1298  ran crn 3987   |` cres 3988  "cima 3989

This theorem is referenced by:  imaeq2i 4262  imaeq2d 4264  relimasn 4288  funimaexg 4495  fnimaOLD 4531  foima 4622  f1imacnv 4656  fvprc 4678  ssimaex 4729  ssimaexg 4730  rdglim 5156  tz7.49 5168  sbthlem2 5511  sbth 5520  ssenen 5598  phplem4 5605  php3 5609  ordtypelem4 5687  ordtypelem5 5688  ordtypelem6 5689  ordtypelem7 5690  zorn2lem6 5955  zorn2lem7 5956  cnpnei 9043  cnima 9044  iscncl 9047  cnclima 9048  cnsscnp 9049  metcnp 9165  uptx 10226  filrn 10293  elfilmap 10312  elfilmap2 10313  elfilmap3 10314  cncomp 10331  oooeqim2 14356  mapudiscn 14872  cmphmp 14878  homcard 14893  eqindhome 14895  conttnf 14944  iscnp3 14946  trhom2 14985  ordtypelem4OLD 15378  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypelem7OLD 15381  cncls 15419  cnntr 15420  cnsubsp2 15427  cnconn 15444  cnpfillim 15589  imaelfm 15591  rnelfmlem 15592  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  filfm 15600  flimfbas 15601  isfclusf 15625  fclsfneii 15628  filnetlem5 15644  filnet 15645  cnimass 15888  cnresima 15891  cnss 15892  hmeoopn 15899  ismtyhmeolem 15950  heiborlem11 15965  heiborlem13 15967

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007

Copyright terms: Public domain