Theorem imaeq2 5892

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 5813	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5772	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5532	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5532	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1538  ran crn 5520   ↾ cres 5521   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  imaeq2i  5894  imaeq2d  5896  relimasn  5919  funimaexg  6410  fimadmfo  6574  ssimaex  6723  ssimaexg  6724  isoselem  7073  isowe2  7082  f1opw2  7380  fnse  7810  supp0cosupp0  7855  supp0cosupp0OLD  7856  tz7.49  8064  ecexr  8277  fopwdom  8608  sbthlem2  8612  sbth  8621  ssenen  8675  domunfican  8775  fodomfi  8781  f1opwfi  8812  fipreima  8814  marypha1lem  8881  ordtypelem2  8967  ordtypelem3  8968  ordtypelem9  8974  dfac12lem2  9555  dfac12r  9557  ackbij2lem2  9651  ackbij2lem3  9652  r1om  9655  enfin2i  9732  zorn2lem6  9912  zorn2lem7  9913  isacs5lem  17771  acsdrscl  17772  gicsubgen  18410  efgrelexlema  18867  tgcn  21857  subbascn  21859  iscnp4  21868  cnpnei  21869  cnima  21870  iscncl  21874  cncls  21879  cnconst2  21888  cnrest2  21891  cnprest  21894  cnindis  21897  cncmp  21997  cmpfi  22013  2ndcomap  22063  ptbasfi  22186  xkoopn  22194  xkoccn  22224  txcnp  22225  ptcnplem  22226  txcnmpt  22229  ptrescn  22244  xkoco1cn  22262  xkoco2cn  22263  xkococn  22265  xkoinjcn  22292  elqtop  22302  qtopomap  22323  qtopcmap  22324  ordthmeolem  22406  fbasrn  22489  elfm  22552  elfm2  22553  elfm3  22555  imaelfm  22556  rnelfmlem  22557  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem3  22561  fmfnfmlem4  22562  fmco  22566  flffbas  22600  lmflf  22610  fcfneii  22642  ptcmplem3  22659  ptcmplem5  22661  ptcmpg  22662  cnextcn  22672  symgtgp  22711  ghmcnp  22720  eltsms  22738  tsmsf1o  22750  fmucnd  22898  ucnextcn  22910  metcnp3  23147  mbfdm  24230  ismbf  24232  mbfima  24234  ismbfd  24243  mbfimaopnlem  24259  mbfimaopn2  24261  i1fd  24285  ellimc2  24480  limcflf  24484  xrlimcnp  25554  ubthlem1  28653  disjpreima  30347  imadifxp  30364  preimane  30433  fnpreimac  30434  qtophaus  31189  rhmpreimacnlem  31237  rrhre  31372  mbfmcnvima  31625  imambfm  31630  eulerpartgbij  31740  erdszelem1  32551  erdsze  32562  erdsze2lem2  32564  cvmscbv  32618  cvmsi  32625  cvmsval  32626  cvmliftlem15  32658  opelco3  33131  brimageg  33501  fnimage  33503  imageval  33504  fvimage  33505  filnetlem4  33842  bj-imdirval3  34599  bj-imdirco  34605  ptrest  35056  ismtyhmeolem  35242  ismtybndlem  35244  heibor1lem  35247  lmhmfgima  40028  brtrclfv2  40428  csbfv12gALTVD  41605  icccncfext  42529  sge0f1o  43021  smfresal  43420  smfpimbor1lem1  43430  smfpimbor1lem2  43431  smfco  43434  imaelsetpreimafv  43912  fundcmpsurinjlem3  43917  imasetpreimafvbijlemfo  43922  fundcmpsurbijinjpreimafv  43924  isomushgr  44344  isomuspgrlem1  44345  isomuspgrlem2a  44346  isomuspgrlem2b  44347  isomuspgrlem2c  44348  isomuspgrlem2d  44349  isomuspgr  44352  isomgrsym  44354