Theorem imaeq2 6004

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 5922	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5877	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5627	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5627	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  ran crn 5615   ↾ cres 5616   “ cima 5617

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627

This theorem is referenced by:  imaeq2i  6006  imaeq2d  6008  relimasn  6033  cnvimassrndm  6099  fimadmfo  6744  ssimaex  6907  ssimaexg  6908  isoselem  7275  isowe2  7284  f1opw2  7601  mptcnfimad  7918  fnse  8063  supp0cosupp0  8138  tz7.49  8364  ecexr  8627  fopwdom  8998  sbthlem2  9001  sbth  9010  ssenen  9064  sbthfi  9108  fodomfi  9196  imafiOLD  9200  domunfican  9206  fodomfiOLD  9214  f1opwfi  9240  fipreima  9242  marypha1lem  9317  ordtypelem2  9405  ordtypelem3  9406  ordtypelem9  9412  dfac12lem2  10036  dfac12r  10038  ackbij2lem2  10130  ackbij2lem3  10131  r1om  10134  enfin2i  10212  zorn2lem6  10392  zorn2lem7  10393  isacs5lem  18451  acsdrscl  18452  gicsubgen  19191  ghmqusnsglem1  19192  ghmquskerlem1  19195  ghmquskerco  19196  gicqusker  19200  efgrelexlema  19661  tgcn  23167  subbascn  23169  iscnp4  23178  cnpnei  23179  cnima  23180  iscncl  23184  cncls  23189  cnconst2  23198  cnrest2  23201  cnprest  23204  cnindis  23207  cncmp  23307  cmpfi  23323  2ndcomap  23373  ptbasfi  23496  xkoopn  23504  xkoccn  23534  txcnp  23535  ptcnplem  23536  txcnmpt  23539  ptrescn  23554  xkoco1cn  23572  xkoco2cn  23573  xkococn  23575  xkoinjcn  23602  elqtop  23612  qtopomap  23633  qtopcmap  23634  ordthmeolem  23716  fbasrn  23799  elfm  23862  elfm2  23863  elfm3  23865  imaelfm  23866  rnelfmlem  23867  rnelfm  23868  fmfnfmlem2  23870  fmfnfmlem3  23871  fmfnfmlem4  23872  fmco  23876  flffbas  23910  lmflf  23920  fcfneii  23952  ptcmplem3  23969  ptcmplem5  23971  ptcmpg  23972  cnextcn  23982  symgtgp  24021  ghmcnp  24030  eltsms  24048  tsmsf1o  24060  fmucnd  24206  ucnextcn  24218  metcnp3  24455  mbfdm  25554  ismbf  25556  mbfima  25558  ismbfd  25567  mbfimaopnlem  25583  mbfimaopn2  25585  i1fd  25609  ellimc2  25805  limcflf  25809  xrlimcnp  26905  oldval  27795  ubthlem1  30850  disjpreima  32564  imadifxp  32581  preimane  32652  fnpreimac  32653  lmicqusker  33383  ricqusker  33392  algextdeglem4  33733  algextdeg  33738  qtophaus  33849  rhmpreimacnlem  33897  rrhre  34034  mbfmcnvima  34268  imambfm  34275  eulerpartgbij  34385  erdszelem1  35235  erdsze  35246  erdsze2lem2  35248  cvmscbv  35302  cvmsi  35309  cvmsval  35310  cvmliftlem15  35342  opelco3  35819  brimageg  35969  fnimage  35971  imageval  35972  fvimage  35973  filnetlem4  36423  bj-imdirval3  37226  bj-imdirco  37232  ptrest  37667  ismtyhmeolem  37852  ismtybndlem  37854  heibor1lem  37857  zndvdchrrhm  42013  aks6d1c7lem2  42222  aks5lem4a  42231  lmhmfgima  43125  brtrclfv2  43768  csbfv12gALTVD  44939  icccncfext  45933  sge0f1o  46428  smfresal  46834  smfpimbor1lem1  46844  smfpimbor1lem2  46845  smfco  46848  f1cof1b  47116  fnfocofob  47118  imaelsetpreimafv  47434  fundcmpsurinjlem3  47439  imasetpreimafvbijlemfo  47444  fundcmpsurbijinjpreimafv  47446  grimco  47928  uhgrimedgi  47929  isuspgrim0  47933  isuspgrimlem  47934  upgrimwlklem5  47940  gricushgr  47956  grimedg  47974  grtrimap  47987  isubgr3stgrlem5  48009  isubgr3stgrlem6  48010  isubgr3stgrlem7  48011  isubgr3stgrlem8  48012  uspgrlimlem4  48030  grlimedgclnbgr  48034  grlimgrtrilem2  48041