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

Theorem imaeq2 5620
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
imaeq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem imaeq2
StepHypRef Expression
1 reseq2 5546 . . 3 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
21rneqd 5508 . 2 (𝐴 = 𝐵 → ran (𝐶𝐴) = ran (𝐶𝐵))
3 df-ima 5279 . 2 (𝐶𝐴) = ran (𝐶𝐴)
4 df-ima 5279 . 2 (𝐶𝐵) = ran (𝐶𝐵)
52, 3, 43eqtr4g 2819 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  ran crn 5267  cres 5268  cima 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279
This theorem is referenced by:  imaeq2i  5622  imaeq2d  5624  relimasn  5646  funimaexg  6136  ssimaex  6425  ssimaexg  6426  isoselem  6754  isowe2  6763  f1opw2  7053  fnse  7462  supp0cosupp0  7503  tz7.49  7709  ecexr  7916  fopwdom  8233  sbthlem2  8236  sbth  8245  ssenen  8299  domunfican  8398  fodomfi  8404  f1opwfi  8435  fipreima  8437  marypha1lem  8504  ordtypelem2  8589  ordtypelem3  8590  ordtypelem9  8596  dfac12lem2  9158  dfac12r  9160  ackbij2lem2  9254  ackbij2lem3  9255  r1om  9258  enfin2i  9335  zorn2lem6  9515  zorn2lem7  9516  isacs5lem  17370  acsdrscl  17371  gicsubgen  17921  efgrelexlema  18362  tgcn  21258  subbascn  21260  iscnp4  21269  cnpnei  21270  cnima  21271  iscncl  21275  cncls  21280  cnconst2  21289  cnrest2  21292  cnprest  21295  cnindis  21298  cncmp  21397  cmpfi  21413  2ndcomap  21463  ptbasfi  21586  xkoopn  21594  xkoccn  21624  txcnp  21625  ptcnplem  21626  txcnmpt  21629  ptrescn  21644  xkoco1cn  21662  xkoco2cn  21663  xkococn  21665  xkoinjcn  21692  elqtop  21702  qtopomap  21723  qtopcmap  21724  ordthmeolem  21806  fbasrn  21889  elfm  21952  elfm2  21953  elfm3  21955  imaelfm  21956  rnelfmlem  21957  rnelfm  21958  fmfnfmlem2  21960  fmfnfmlem3  21961  fmfnfmlem4  21962  fmco  21966  flffbas  22000  lmflf  22010  fcfneii  22042  ptcmplem3  22059  ptcmplem5  22061  ptcmpg  22062  cnextcn  22072  symgtgp  22106  ghmcnp  22119  eltsms  22137  tsmsf1o  22149  fmucnd  22297  ucnextcn  22309  metcnp3  22546  mbfdm  23594  ismbf  23596  mbfima  23598  ismbfd  23606  mbfimaopnlem  23621  mbfimaopn2  23623  i1fd  23647  ellimc2  23840  limcflf  23844  xrlimcnp  24894  ubthlem1  28035  disjpreima  29704  imadifxp  29721  qtophaus  30212  rrhre  30374  mbfmcnvima  30628  imambfm  30633  eulerpartgbij  30743  erdszelem1  31480  erdsze  31491  erdsze2lem2  31493  cvmscbv  31547  cvmsi  31554  cvmsval  31555  cvmliftlem15  31587  opelco3  31983  brimageg  32340  fnimage  32342  imageval  32343  fvimage  32344  filnetlem4  32682  ptrest  33721  ismtyhmeolem  33916  ismtybndlem  33918  heibor1lem  33921  lmhmfgima  38156  brtrclfv2  38521  csbfv12gALTVD  39634  icccncfext  40603  sge0f1o  41102  smfresal  41501  smfpimbor1lem1  41511  smfpimbor1lem2  41512  smfco  41515
  Copyright terms: Public domain W3C validator