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

Theorem imaeq2 5132
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 5074 . . 3  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
21rneqd 5030 . 2  |-  ( A  =  B  ->  ran  ( C  |`  A )  =  ran  ( C  |`  B ) )
3 df-ima 4824 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
4 df-ima 4824 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
52, 3, 43eqtr4g 2437 1  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ran crn 4812    |` cres 4813   "cima 4814
This theorem is referenced by:  imaeq2i  5134  imaeq2d  5136  relimasn  5160  funimaexg  5463  ssimaex  5720  ssimaexg  5721  isoselem  5993  isowe2  6002  f1opw2  6230  fnse  6392  tz7.49  6631  ecexr  6839  fopwdom  7145  sbthlem2  7147  sbth  7156  ssenen  7210  domunfican  7308  fodomfi  7314  f1opwfi  7338  fipreima  7340  marypha1lem  7366  ordtypelem2  7414  ordtypelem3  7415  ordtypelem9  7421  dfac12lem2  7950  dfac12r  7952  ackbij2lem2  8046  ackbij2lem3  8047  r1om  8050  enfin2i  8127  zorn2lem6  8307  zorn2lem7  8308  isacs5lem  14515  acsdrscl  14516  gicsubgen  14985  efgrelexlema  15301  gsumval3  15434  tgcn  17231  subbascn  17233  iscnp4  17242  cnpnei  17243  cnima  17244  iscncl  17248  cncls  17253  cnconst2  17262  cnrest2  17265  cnprest  17268  cnindis  17271  cncmp  17370  cmpfi  17386  2ndcomap  17435  ptbasfi  17527  xkoopn  17535  xkoccn  17565  txcnp  17566  ptcnplem  17567  txcnmpt  17570  ptrescn  17585  xkoco1cn  17603  xkoco2cn  17604  xkococn  17606  xkoinjcn  17633  elqtop  17643  qtopomap  17664  qtopcmap  17665  ordthmeolem  17747  fbasrn  17830  elfm  17893  elfm2  17894  elfm3  17896  imaelfm  17897  rnelfmlem  17898  rnelfm  17899  fmfnfmlem2  17901  fmfnfmlem3  17902  fmfnfmlem4  17903  fmco  17907  flffbas  17941  lmflf  17951  fcfneii  17983  ptcmplem3  17999  ptcmplem5  18001  ptcmpg  18002  cnextcn  18012  symgtgp  18045  ghmcnp  18058  eltsms  18076  tsmsf1o  18088  fmucnd  18236  ucnextcn  18248  metcnp3  18453  mbfdm  19380  ismbf  19382  mbfima  19384  ismbfd  19392  mbfimaopnlem  19407  mbfimaopn2  19409  i1fd  19433  ellimc2  19624  limcflf  19628  xrlimcnp  20667  ubthlem1  22213  disjpreima  23863  imadifxp  23874  rrhre  24176  mbfmcnvima  24394  imambfm  24399  erdszelem1  24649  erdsze  24660  erdsze2lem2  24662  cvmscbv  24717  cvmsi  24724  cvmsval  24725  cvmliftlem15  24757  brimageg  25483  fnimage  25485  imageval  25486  fvimage  25487  filnetlem4  26094  ismtyhmeolem  26197  ismtybndlem  26199  heibor1lem  26202  lmhmfgima  26844  csbfv12gALTVD  28345
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-br 4147  df-opab 4201  df-xp 4817  df-cnv 4819  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824
  Copyright terms: Public domain W3C validator