Theorem imaeq12d 6068

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 6066	. 2 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3		imaeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	imaeq2d 6067	. 2 ⊢ (𝜑 → (𝐵 “ 𝐶) = (𝐵 “ 𝐷))
5	2, 4	eqtrd 2801	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   “ cima 5669

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is used by:  csbima12  6086  predeq123  6310  vdwpc  17065  dmdprd  20101  isunit  20488  qtopval  23889  limciun  26090  ig1pval  26370  ispth  30107  esplyval  33983  irngval  34106  qqhval  34393  eulerpartgbij  34794  orvcval  34880  ballotlemrval  34940  ballotlemrinv0  34955  ballotlemrinv  34956  mthmval  36088  bj-projeq  37669  itg2addnclem2  38364  islmodfg  43837  heeq12  44543  isgrim  48688  imaf1hom  49927  imaidfu  49929  imasubc  49970  imassc  49972  imaid  49973