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

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

Proof of Theorem imaeq2
StepHypRef Expression
1 reseq2 5423 . . 3 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
21rneqd 5385 . 2 (𝐴 = 𝐵 → ran (𝐶𝐴) = ran (𝐶𝐵))
3 df-ima 5156 . 2 (𝐶𝐴) = ran (𝐶𝐴)
4 df-ima 5156 . 2 (𝐶𝐵) = ran (𝐶𝐵)
52, 3, 43eqtr4g 2710 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ran crn 5144  cres 5145  cima 5146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-cnv 5151  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156
This theorem is referenced by:  imaeq2i  5499  imaeq2d  5501  relimasn  5523  funimaexg  6013  ssimaex  6302  ssimaexg  6303  isoselem  6631  isowe2  6640  f1opw2  6930  fnse  7339  supp0cosupp0  7379  tz7.49  7585  ecexr  7792  fopwdom  8109  sbthlem2  8112  sbth  8121  ssenen  8175  domunfican  8274  fodomfi  8280  f1opwfi  8311  fipreima  8313  marypha1lem  8380  ordtypelem2  8465  ordtypelem3  8466  ordtypelem9  8472  dfac12lem2  9004  dfac12r  9006  ackbij2lem2  9100  ackbij2lem3  9101  r1om  9104  enfin2i  9181  zorn2lem6  9361  zorn2lem7  9362  isacs5lem  17216  acsdrscl  17217  gicsubgen  17767  efgrelexlema  18208  tgcn  21104  subbascn  21106  iscnp4  21115  cnpnei  21116  cnima  21117  iscncl  21121  cncls  21126  cnconst2  21135  cnrest2  21138  cnprest  21141  cnindis  21144  cncmp  21243  cmpfi  21259  2ndcomap  21309  ptbasfi  21432  xkoopn  21440  xkoccn  21470  txcnp  21471  ptcnplem  21472  txcnmpt  21475  ptrescn  21490  xkoco1cn  21508  xkoco2cn  21509  xkococn  21511  xkoinjcn  21538  elqtop  21548  qtopomap  21569  qtopcmap  21570  ordthmeolem  21652  fbasrn  21735  elfm  21798  elfm2  21799  elfm3  21801  imaelfm  21802  rnelfmlem  21803  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem3  21807  fmfnfmlem4  21808  fmco  21812  flffbas  21846  lmflf  21856  fcfneii  21888  ptcmplem3  21905  ptcmplem5  21907  ptcmpg  21908  cnextcn  21918  symgtgp  21952  ghmcnp  21965  eltsms  21983  tsmsf1o  21995  fmucnd  22143  ucnextcn  22155  metcnp3  22392  mbfdm  23440  ismbf  23442  mbfima  23444  ismbfd  23452  mbfimaopnlem  23467  mbfimaopn2  23469  i1fd  23493  ellimc2  23686  limcflf  23690  xrlimcnp  24740  ubthlem1  27854  disjpreima  29523  imadifxp  29540  qtophaus  30031  rrhre  30193  mbfmcnvima  30447  imambfm  30452  eulerpartgbij  30562  erdszelem1  31299  erdsze  31310  erdsze2lem2  31312  cvmscbv  31366  cvmsi  31373  cvmsval  31374  cvmliftlem15  31406  opelco3  31802  brimageg  32159  fnimage  32161  imageval  32162  fvimage  32163  filnetlem4  32501  ptrest  33538  ismtyhmeolem  33733  ismtybndlem  33735  heibor1lem  33738  lmhmfgima  37971  brtrclfv2  38336  csbfv12gALTVD  39449  icccncfext  40418  sge0f1o  40917  smfresal  41316  smfpimbor1lem1  41326  smfpimbor1lem2  41327  smfco  41330
  Copyright terms: Public domain W3C validator