MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaeq2 Unicode version

Theorem imaeq2 5166
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
StepHypRef Expression
1 reseq2 5108 . . 3  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
21rneqd 5064 . 2  |-  ( A  =  B  ->  ran  ( C  |`  A )  =  ran  ( C  |`  B ) )
3 df-ima 4858 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
4 df-ima 4858 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
52, 3, 43eqtr4g 2469 1  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ran crn 4846    |` cres 4847   "cima 4848
This theorem is referenced by:  imaeq2i  5168  imaeq2d  5170  relimasn  5194  funimaexg  5497  ssimaex  5755  ssimaexg  5756  isoselem  6028  isowe2  6037  f1opw2  6265  fnse  6430  tz7.49  6669  ecexr  6877  fopwdom  7183  sbthlem2  7185  sbth  7194  ssenen  7248  domunfican  7346  fodomfi  7352  f1opwfi  7376  fipreima  7378  marypha1lem  7404  ordtypelem2  7452  ordtypelem3  7453  ordtypelem9  7459  dfac12lem2  7988  dfac12r  7990  ackbij2lem2  8084  ackbij2lem3  8085  r1om  8088  enfin2i  8165  zorn2lem6  8345  zorn2lem7  8346  isacs5lem  14558  acsdrscl  14559  gicsubgen  15028  efgrelexlema  15344  gsumval3  15477  tgcn  17278  subbascn  17280  iscnp4  17289  cnpnei  17290  cnima  17291  iscncl  17295  cncls  17300  cnconst2  17309  cnrest2  17312  cnprest  17315  cnindis  17318  cncmp  17417  cmpfi  17433  2ndcomap  17482  ptbasfi  17574  xkoopn  17582  xkoccn  17612  txcnp  17613  ptcnplem  17614  txcnmpt  17617  ptrescn  17632  xkoco1cn  17650  xkoco2cn  17651  xkococn  17653  xkoinjcn  17680  elqtop  17690  qtopomap  17711  qtopcmap  17712  ordthmeolem  17794  fbasrn  17877  elfm  17940  elfm2  17941  elfm3  17943  imaelfm  17944  rnelfmlem  17945  rnelfm  17946  fmfnfmlem2  17948  fmfnfmlem3  17949  fmfnfmlem4  17950  fmco  17954  flffbas  17988  lmflf  17998  fcfneii  18030  ptcmplem3  18046  ptcmplem5  18048  ptcmpg  18049  cnextcn  18059  symgtgp  18092  ghmcnp  18105  eltsms  18123  tsmsf1o  18135  fmucnd  18283  ucnextcn  18295  metcnp3  18531  mbfdm  19481  ismbf  19483  mbfima  19485  ismbfd  19493  mbfimaopnlem  19508  mbfimaopn2  19510  i1fd  19534  ellimc2  19725  limcflf  19729  xrlimcnp  20768  ubthlem1  22333  disjpreima  23987  imadifxp  23999  rrhre  24348  mbfmcnvima  24568  imambfm  24573  erdszelem1  24838  erdsze  24849  erdsze2lem2  24851  cvmscbv  24906  cvmsi  24913  cvmsval  24914  cvmliftlem15  24946  brimageg  25688  fnimage  25690  imageval  25691  fvimage  25692  filnetlem4  26308  ismtyhmeolem  26411  ismtybndlem  26413  heibor1lem  26416  lmhmfgima  27058  csbfv12gALTVD  28729
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181  df-opab 4235  df-xp 4851  df-cnv 4853  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858
  Copyright terms: Public domain W3C validator