Metamath Proof Explorer

Theorem uneq12i

Description: Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004) (Proof shortened by Eric Schmidt, 26-Jan-2007)

Ref Expression
Hypotheses uneq1i.1 A = B
uneq12i.2 C = D
Assertion uneq12i A C = B D


Step Hyp Ref Expression
1 uneq1i.1 A = B
2 uneq12i.2 C = D
3 uneq12 A = B C = D A C = B D
4 1 2 3 mp2an A C = B D