Theorem imaeq12d 6020

Description: Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)

Hypotheses

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
imaeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

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

Proof of Theorem imaeq12d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	imaeq1d 6018	. 2 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3		imaeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	imaeq2d 6019	. 2 ⊢ (𝜑 → (𝐵 “ 𝐶) = (𝐵 “ 𝐷))
5	2, 4	eqtrd 2775	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))

Syntax hints:   → wi 4   = wceq 1547   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  csbima12  6038  predeq123  6260  vdwpc  16949  dmdprd  19973  isunit  20351  qtopval  23685  limciun  25886  ig1pval  26166  ispth  29814  esplyval  33753  irngval  33876  qqhval  34163  eulerpartgbij  34563  orvcval  34649  ballotlemrval  34709  ballotlemrinv0  34724  ballotlemrinv  34725  mthmval  35810  bj-projeq  37352  itg2addnclem2  38046  islmodfg  43521  heeq12  44227  isgrim  48380  imaf1hom  49605  imaidfu  49607  imasubc  49648  imassc  49650  imaid  49651