Theorem imaeq1 5461

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

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

Proof of Theorem imaeq1

Step	Hyp	Ref	Expression
1		reseq1 5390	. . 3 |- ( A = B -> ( A |` C ) = ( B |` C ) )
2	1	rneqd 5353	. 2 |- ( A = B -> ran ( A |` C ) = ran ( B |` C ) )
3		df-ima 5127	. 2 |- ( A " C ) = ran ( A |` C )
4		df-ima 5127	. 2 |- ( B " C ) = ran ( B |` C )
5	2, 3, 4	3eqtr4g 2681	1 |- ( A = B -> ( A " C ) = ( B " C ) )

Syntax hints:   -> wi 4   = wceq 1483   ran crn 5115   |` cres 5116   "cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  imaeq1i  5463  imaeq1d  5465  suppval  7297  eceq2  7784  marypha1lem  8339  marypha1  8340  ackbij2lem2  9062  ackbij2lem3  9063  r1om  9066  limsupval  14205  isacs1i  16318  mreacs  16319  islindf  20151  iscnp  21041  xkoccn  21422  xkohaus  21456  xkoco1cn  21460  xkoco2cn  21461  xkococnlem  21462  xkococn  21463  xkoinjcn  21490  fmval  21747  fmf  21749  utoptop  22038  restutop  22041  restutopopn  22042  ustuqtoplem  22043  ustuqtop1  22045  ustuqtop2  22046  ustuqtop4  22048  ustuqtop5  22049  utopsnneiplem  22051  utopsnnei  22053  neipcfilu  22100  psmetutop  22372  cfilfval  23062  elply2  23952  coeeu  23981  coelem  23982  coeeq  23983  dmarea  24684  mclsax  31466  tailfval  32367  bj-cleq  32949  poimirlem15  33424  poimirlem24  33433  brtrclfv2  38019  liminfval  39991