Theorem imaeq2 6059

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 5974	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5929	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5675	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5675	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2829	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1567  ran crn 5663   ↾ cres 5664   “ cima 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  imaeq2i  6061  imaeq2d  6063  relimasn  6088  cnvimassrndm  6150  fimadmfo  6802  ssimaex  6967  ssimaexg  6968  isoselem  7340  isowe2  7349  f1opw2  7666  mptcnfimad  7983  fnse  8129  supp0cosupp0  8204  tz7.49  8432  ecexr  8699  fopwdom  9073  sbthlem2  9076  sbth  9085  ssenen  9139  sbthfi  9183  fodomfi  9272  domunfican  9281  f1opwfi  9313  fipreima  9315  marypha1lem  9393  ordtypelem2  9481  ordtypelem3  9482  ordtypelem9  9488  dfac12lem2  10128  dfac12r  10130  ackbij2lem2  10222  ackbij2lem3  10223  r1om  10226  enfin2i  10305  zorn2lem6  10485  zorn2lem7  10486  isacs5lem  18601  acsdrscl  18602  gicsubgen  19349  ghmqusnsglem1  19350  ghmquskerlem1  19353  ghmquskerco  19354  gicqusker  19358  efgrelexlema  19819  tgcn  23378  subbascn  23380  iscnp4  23389  cnpnei  23390  cnima  23391  iscncl  23395  cncls  23400  cnconst2  23409  cnrest2  23412  cnprest  23415  cnindis  23418  cncmp  23518  cmpfi  23534  2ndcomap  23584  ptbasfi  23707  xkoopn  23715  xkoccn  23745  txcnp  23746  ptcnplem  23747  txcnmpt  23750  ptrescn  23765  xkoco1cn  23783  xkoco2cn  23784  xkococn  23786  xkoinjcn  23813  elqtop  23823  qtopomap  23844  qtopcmap  23845  ordthmeolem  23927  fbasrn  24010  elfm  24073  elfm2  24074  elfm3  24076  imaelfm  24077  rnelfmlem  24078  rnelfm  24079  fmfnfmlem2  24081  fmfnfmlem3  24082  fmfnfmlem4  24083  fmco  24087  flffbas  24121  lmflf  24131  fcfneii  24163  ptcmplem3  24180  ptcmplem5  24182  ptcmpg  24183  cnextcn  24193  symgtgp  24232  ghmcnp  24241  eltsms  24259  tsmsf1o  24271  fmucnd  24417  ucnextcn  24429  metcnp3  24666  mbfdm  25754  ismbf  25756  mbfima  25758  ismbfd  25767  mbfimaopnlem  25783  mbfimaopn2  25785  i1fd  25809  ellimc2  26005  limcflf  26009  xrlimcnp  27099  oldval  27993  ubthlem1  31163  disjpreima  32870  imadifxp  32887  preimane  32955  fnpreimac  32956  lmicqusker  33671  ricqusker  33679  algextdeglem4  34055  algextdeg  34060  qtophaus  34171  rhmpreimacnlem  34219  rrhre  34356  mbfmcnvima  34590  imambfm  34597  eulerpartgbij  34707  erdszelem1  35582  erdsze  35593  erdsze2lem2  35595  cvmscbv  35649  cvmsi  35656  cvmsval  35657  cvmliftlem15  35689  opelco3  36166  brimageg  36316  fnimage  36318  imageval  36319  fvimage  36320  filnetlem4  36781  bj-imdirval3  37716  bj-imdirco  37722  ptrest  38158  ismtyhmeolem  38343  ismtybndlem  38345  heibor1lem  38348  zndvdchrrhm  42630  aks6d1c7lem2  42838  aks5lem4a  42847  lmhmfgima  43703  brtrclfv2  44345  csbfv12gALTVD  45499  icccncfext  46493  sge0f1o  46988  smfresal  47394  smfpimbor1lem1  47404  smfpimbor1lem2  47405  smfco  47408  f1cof1b  47703  fnfocofob  47705  imaelsetpreimafv  48033  fundcmpsurinjlem3  48038  imasetpreimafvbijlemfo  48043  fundcmpsurbijinjpreimafv  48045  grimco  48543  uhgrimedgi  48544  isuspgrim0  48548  isuspgrimlem  48549  upgrimwlklem5  48555  gricushgr  48571  grimedg  48589  grtrimap  48602  isubgr3stgrlem5  48624  isubgr3stgrlem6  48625  isubgr3stgrlem7  48626  isubgr3stgrlem8  48627  uspgrlimlem4  48645  grlimedgclnbgr  48649  grlimgrtrilem2  48656