Theorem imaeq2 6056

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 5977	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5938	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5690	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5690	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1542  ran crn 5678   ↾ cres 5679   “ cima 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690

This theorem is referenced by:  imaeq2i  6058  imaeq2d  6060  relimasn  6084  cnvimassrndm  6152  funimaexgOLD  6636  fimadmfo  6815  ssimaex  6977  ssimaexg  6978  isoselem  7338  isowe2  7347  f1opw2  7661  fnse  8119  supp0cosupp0  8193  tz7.49  8445  ecexr  8708  fopwdom  9080  sbthlem2  9084  sbth  9093  ssenen  9151  imafi  9175  sbthfi  9202  domunfican  9320  fodomfi  9325  f1opwfi  9356  fipreima  9358  marypha1lem  9428  ordtypelem2  9514  ordtypelem3  9515  ordtypelem9  9521  dfac12lem2  10139  dfac12r  10141  ackbij2lem2  10235  ackbij2lem3  10236  r1om  10239  enfin2i  10316  zorn2lem6  10496  zorn2lem7  10497  isacs5lem  18498  acsdrscl  18499  gicsubgen  19152  efgrelexlema  19617  tgcn  22756  subbascn  22758  iscnp4  22767  cnpnei  22768  cnima  22769  iscncl  22773  cncls  22778  cnconst2  22787  cnrest2  22790  cnprest  22793  cnindis  22796  cncmp  22896  cmpfi  22912  2ndcomap  22962  ptbasfi  23085  xkoopn  23093  xkoccn  23123  txcnp  23124  ptcnplem  23125  txcnmpt  23128  ptrescn  23143  xkoco1cn  23161  xkoco2cn  23162  xkococn  23164  xkoinjcn  23191  elqtop  23201  qtopomap  23222  qtopcmap  23223  ordthmeolem  23305  fbasrn  23388  elfm  23451  elfm2  23452  elfm3  23454  imaelfm  23455  rnelfmlem  23456  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem3  23460  fmfnfmlem4  23461  fmco  23465  flffbas  23499  lmflf  23509  fcfneii  23541  ptcmplem3  23558  ptcmplem5  23560  ptcmpg  23561  cnextcn  23571  symgtgp  23610  ghmcnp  23619  eltsms  23637  tsmsf1o  23649  fmucnd  23797  ucnextcn  23809  metcnp3  24049  mbfdm  25143  ismbf  25145  mbfima  25147  ismbfd  25156  mbfimaopnlem  25172  mbfimaopn2  25174  i1fd  25198  ellimc2  25394  limcflf  25398  xrlimcnp  26473  oldval  27349  ubthlem1  30123  disjpreima  31815  imadifxp  31832  preimane  31895  fnpreimac  31896  ghmquskerlem1  32528  ghmquskerco  32529  gicqusker  32533  lmicqusker  32535  ricqusker  32545  algextdeglem1  32772  qtophaus  32816  rhmpreimacnlem  32864  rrhre  33001  mbfmcnvima  33254  imambfm  33261  eulerpartgbij  33371  erdszelem1  34182  erdsze  34193  erdsze2lem2  34195  cvmscbv  34249  cvmsi  34256  cvmsval  34257  cvmliftlem15  34289  opelco3  34746  brimageg  34899  fnimage  34901  imageval  34902  fvimage  34903  filnetlem4  35266  bj-imdirval3  36065  bj-imdirco  36071  ptrest  36487  ismtyhmeolem  36672  ismtybndlem  36674  heibor1lem  36677  lmhmfgima  41826  brtrclfv2  42478  csbfv12gALTVD  43660  icccncfext  44603  sge0f1o  45098  smfresal  45504  smfpimbor1lem1  45514  smfpimbor1lem2  45515  smfco  45518  f1cof1b  45785  fnfocofob  45787  imaelsetpreimafv  46063  fundcmpsurinjlem3  46068  imasetpreimafvbijlemfo  46073  fundcmpsurbijinjpreimafv  46075  isomushgr  46494  isomuspgrlem1  46495  isomuspgrlem2a  46496  isomuspgrlem2b  46497  isomuspgrlem2c  46498  isomuspgrlem2d  46499  isomuspgr  46502  isomgrsym  46504