Theorem imaeq2 5142

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 5078	. . 3 |- ( A = B -> ( C |` A ) = ( C |` B ) )
2	1	rneqd 5040	. 2 |- ( A = B -> ran ( C |` A ) = ran ( C |` B ) )
3		df-ima 4825	. 2 |- ( C " A ) = ran ( C |` A )
4		df-ima 4825	. 2 |- ( C " B ) = ran ( C |` B )
5	2, 3, 4	3eqtr4g 2511	1 |- ( A = B -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1448   ran crn 4813   |` cres 4814   "cima 4815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4375  df-opab 4434  df-xp 4818  df-cnv 4820  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825

This theorem is referenced by:  imaeq2i  5144  imaeq2d  5146  relimasn  5169  funimaexg  5642  ssimaex  5914  ssimaexg  5915  isoselem  6218  isowe2  6227  f1opw2  6510  fnse  6901  supp0cosupp0  6942  tz7.49  7149  ecexr  7355  fopwdom  7667  sbthlem2  7670  sbth  7679  ssenen  7733  domunfican  7831  fodomfi  7837  f1opwfi  7865  fipreima  7867  marypha1lem  7934  ordtypelem2  8021  ordtypelem3  8022  ordtypelem9  8028  dfac12lem2  8561  dfac12r  8563  ackbij2lem2  8657  ackbij2lem3  8658  r1om  8661  enfin2i  8738  zorn2lem6  8918  zorn2lem7  8919  isacs5lem  16426  acsdrscl  16427  gicsubgen  16953  efgrelexlema  17410  tgcn  20279  subbascn  20281  iscnp4  20290  cnpnei  20291  cnima  20292  iscncl  20296  cncls  20301  cnconst2  20310  cnrest2  20313  cnprest  20316  cnindis  20319  cncmp  20418  cmpfi  20434  2ndcomap  20484  ptbasfi  20607  xkoopn  20615  xkoccn  20645  txcnp  20646  ptcnplem  20647  txcnmpt  20650  ptrescn  20665  xkoco1cn  20683  xkoco2cn  20684  xkococn  20686  xkoinjcn  20713  elqtop  20723  qtopomap  20744  qtopcmap  20745  ordthmeolem  20827  fbasrn  20910  elfm  20973  elfm2  20974  elfm3  20976  imaelfm  20977  rnelfmlem  20978  rnelfm  20979  fmfnfmlem2  20981  fmfnfmlem3  20982  fmfnfmlem4  20983  fmco  20987  flffbas  21021  lmflf  21031  fcfneii  21063  ptcmplem3  21080  ptcmplem5  21082  ptcmpg  21083  cnextcn  21093  symgtgp  21127  ghmcnp  21140  eltsms  21158  tsmsf1o  21170  fmucnd  21318  ucnextcn  21330  metcnp3  21566  mbfdm  22596  ismbf  22598  mbfima  22600  ismbfd  22608  mbfimaopnlem  22623  mbfimaopn2  22625  i1fd  22651  ellimc2  22844  limcflf  22848  xrlimcnp  23906  ubthlem1  26524  disjpreima  28204  imadifxp  28221  qtophaus  28670  rrhre  28832  mbfmcnvima  29085  imambfm  29090  eulerpartgbij  29211  erdszelem1  29920  erdsze  29931  erdsze2lem2  29933  cvmscbv  29987  cvmsi  29994  cvmsval  29995  cvmliftlem15  30027  opelco3  30426  brimageg  30700  fnimage  30702  imageval  30703  fvimage  30704  filnetlem4  31043  ptrest  31941  ismtyhmeolem  32138  ismtybndlem  32140  heibor1lem  32143  lmhmfgima  35944  brtrclfv2  36321  csbfv12gALTVD  37293  icccncfext  37807  sge0f1o  38283