Theorem imaeq2d 5108

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq2d	⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq2 5104	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1398   “ cima 4759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3701  df-pr 3702  df-op 3704  df-br 4116  df-opab 4178  df-xp 4762  df-cnv 4764  df-dm 4766  df-rn 4767  df-res 4768  df-ima 4769

This theorem is referenced by:  imaeq12d  5109  nfimad  5117  elimasng  5137  ressn  5310  foima  5602  f1imacnv  5638  fvco2  5753  fsn2  5858  fncofn  5869  resfunexg  5912  funfvima3  5927  funiunfvdm  5944  isoselem  6001  fnexALT  6315  suppsnopdc  6465  suppcofn  6481  imacosuppfn  6483  eceq1  6817  uniqs2  6844  ecinxp  6859  mapsnd  6938  mapsn  6940  en2  7080  phplem4  7124  phplem4dom  7131  phplem4on  7137  sbthlem2  7243  isbth  7252  resunimafz0  11228  ballotfilemscr  13212  ennnfonelemg  13244  ennnfonelemhf1o  13254  ennnfonelemex  13255  ennnfonelemrn  13260  cnntr  15222  cnptopresti  15235  cnptoprest  15236  eupth2lem3fi  16603  eupth2fi  16606