Theorem imaeq2 5927

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq2	⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 5850	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5810	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5570	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5570	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2883	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1537  ran crn 5558   ↾ cres 5559   “ cima 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  imaeq2i  5929  imaeq2d  5931  relimasn  5954  funimaexg  6442  fimadmfo  6601  ssimaex  6750  ssimaexg  6751  isoselem  7096  isowe2  7105  f1opw2  7402  fnse  7829  supp0cosupp0  7874  supp0cosupp0OLD  7875  tz7.49  8083  ecexr  8296  fopwdom  8627  sbthlem2  8630  sbth  8639  ssenen  8693  domunfican  8793  fodomfi  8799  f1opwfi  8830  fipreima  8832  marypha1lem  8899  ordtypelem2  8985  ordtypelem3  8986  ordtypelem9  8992  dfac12lem2  9572  dfac12r  9574  ackbij2lem2  9664  ackbij2lem3  9665  r1om  9668  enfin2i  9745  zorn2lem6  9925  zorn2lem7  9926  isacs5lem  17781  acsdrscl  17782  gicsubgen  18420  efgrelexlema  18877  tgcn  21862  subbascn  21864  iscnp4  21873  cnpnei  21874  cnima  21875  iscncl  21879  cncls  21884  cnconst2  21893  cnrest2  21896  cnprest  21899  cnindis  21902  cncmp  22002  cmpfi  22018  2ndcomap  22068  ptbasfi  22191  xkoopn  22199  xkoccn  22229  txcnp  22230  ptcnplem  22231  txcnmpt  22234  ptrescn  22249  xkoco1cn  22267  xkoco2cn  22268  xkococn  22270  xkoinjcn  22297  elqtop  22307  qtopomap  22328  qtopcmap  22329  ordthmeolem  22411  fbasrn  22494  elfm  22557  elfm2  22558  elfm3  22560  imaelfm  22561  rnelfmlem  22562  rnelfm  22563  fmfnfmlem2  22565  fmfnfmlem3  22566  fmfnfmlem4  22567  fmco  22571  flffbas  22605  lmflf  22615  fcfneii  22647  ptcmplem3  22664  ptcmplem5  22666  ptcmpg  22667  cnextcn  22677  symgtgp  22716  ghmcnp  22725  eltsms  22743  tsmsf1o  22755  fmucnd  22903  ucnextcn  22915  metcnp3  23152  mbfdm  24229  ismbf  24231  mbfima  24233  ismbfd  24242  mbfimaopnlem  24258  mbfimaopn2  24260  i1fd  24284  ellimc2  24477  limcflf  24481  xrlimcnp  25548  ubthlem1  28649  disjpreima  30336  imadifxp  30353  preimane  30417  fnpreimac  30418  qtophaus  31102  rrhre  31264  mbfmcnvima  31517  imambfm  31522  eulerpartgbij  31632  erdszelem1  32440  erdsze  32451  erdsze2lem2  32453  cvmscbv  32507  cvmsi  32514  cvmsval  32515  cvmliftlem15  32547  opelco3  33020  brimageg  33390  fnimage  33392  imageval  33393  fvimage  33394  filnetlem4  33731  bj-imdirval3  34476  ptrest  34893  ismtyhmeolem  35084  ismtybndlem  35086  heibor1lem  35089  lmhmfgima  39691  brtrclfv2  40079  csbfv12gALTVD  41240  icccncfext  42177  sge0f1o  42671  smfresal  43070  smfpimbor1lem1  43080  smfpimbor1lem2  43081  smfco  43084  imaelsetpreimafv  43562  fundcmpsurinjlem3  43567  imasetpreimafvbijlemfo  43572  fundcmpsurbijinjpreimafv  43574  isomushgr  43998  isomuspgrlem1  43999  isomuspgrlem2a  44000  isomuspgrlem2b  44001  isomuspgrlem2c  44002  isomuspgrlem2d  44003  isomuspgr  44006  isomgrsym  44008