Theorem imaeq2 5258

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 5194	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5156	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4939	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4939	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2458	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1399   ran crn 4927   |` cres 4928   "cima 4929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-br 4381  df-opab 4439  df-xp 4932  df-cnv 4934  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939

This theorem is referenced by:  imaeq2i  5260  imaeq2d  5262  relimasn  5285  funimaexg  5586  ssimaex  5852  ssimaexg  5853  isoselem  6156  isowe2  6165  f1opw2  6445  fnse  6834  supp0cosupp0  6875  tz7.49  7046  ecexr  7252  fopwdom  7562  sbthlem2  7565  sbth  7574  ssenen  7628  domunfican  7726  fodomfi  7732  f1opwfi  7757  fipreima  7759  marypha1lem  7826  ordtypelem2  7877  ordtypelem3  7878  ordtypelem9  7884  dfac12lem2  8455  dfac12r  8457  ackbij2lem2  8551  ackbij2lem3  8552  r1om  8555  enfin2i  8632  zorn2lem6  8812  zorn2lem7  8813  isacs5lem  15935  acsdrscl  15936  gicsubgen  16462  efgrelexlema  16903  gsumval3OLD  17044  tgcn  19858  subbascn  19860  iscnp4  19869  cnpnei  19870  cnima  19871  iscncl  19875  cncls  19880  cnconst2  19889  cnrest2  19892  cnprest  19895  cnindis  19898  cncmp  19997  cmpfi  20013  2ndcomap  20063  ptbasfi  20186  xkoopn  20194  xkoccn  20224  txcnp  20225  ptcnplem  20226  txcnmpt  20229  ptrescn  20244  xkoco1cn  20262  xkoco2cn  20263  xkococn  20265  xkoinjcn  20292  elqtop  20302  qtopomap  20323  qtopcmap  20324  ordthmeolem  20406  fbasrn  20489  elfm  20552  elfm2  20553  elfm3  20555  imaelfm  20556  rnelfmlem  20557  rnelfm  20558  fmfnfmlem2  20560  fmfnfmlem3  20561  fmfnfmlem4  20562  fmco  20566  flffbas  20600  lmflf  20610  fcfneii  20642  ptcmplem3  20658  ptcmplem5  20660  ptcmpg  20661  cnextcn  20671  symgtgp  20704  ghmcnp  20717  eltsms  20735  tsmsf1o  20751  fmucnd  20899  ucnextcn  20911  metcnp3  21147  mbfdm  22139  ismbf  22141  mbfima  22143  ismbfd  22151  mbfimaopnlem  22166  mbfimaopn2  22168  i1fd  22192  ellimc2  22385  limcflf  22389  xrlimcnp  23434  ubthlem1  25924  disjpreima  27603  imadifxp  27621  qtophaus  28024  rrhre  28183  mbfmcnvima  28420  imambfm  28425  eulerpartgbij  28530  erdszelem1  28860  erdsze  28871  erdsze2lem2  28873  cvmscbv  28928  cvmsi  28935  cvmsval  28936  cvmliftlem15  28968  opelco3  29409  brimageg  29766  fnimage  29768  imageval  29769  fvimage  29770  ptrest  30249  filnetlem4  30401  ismtyhmeolem  30502  ismtybndlem  30504  heibor1lem  30507  lmhmfgima  31232  icccncfext  31891  csbfv12gALTVD  34081  brtrclfv2  38293