Theorem imaeq2 5006

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 4942	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 4896	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4677	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4677	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2254	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1364   ran crn 4665   |` cres 4666   "cima 4667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035  df-opab 4096  df-xp 4670  df-cnv 4672  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677

This theorem is referenced by:  imaeq2i  5008  imaeq2d  5010  fimadmfo  5492  ssimaex  5625  ssimaexg  5626  isoselem  5870  f1opw2  6133  fopwdom  6906  ssenen  6921  fiintim  7001  fidcenumlemrk  7029  fidcenumlemr  7030  sbthlem2  7033  isbth  7042  ennnfonelemp1  12648  ennnfonelemnn0  12664  ctinfomlemom  12669  ctinfom  12670  tgcn  14528  iscnp4  14538  cnpnei  14539  cnima  14540  cnconst2  14553  cnrest2  14556  cnptoprest  14559  txcnp  14591  txcnmpt  14593  metcnp3  14831