Metamath Proof Explorer


Theorem iuneq2i

Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003)

Ref Expression
Hypothesis iuneq2i.1 x A B = C
Assertion iuneq2i x A B = x A C

Proof

Step Hyp Ref Expression
1 iuneq2i.1 x A B = C
2 iuneq2 x A B = C x A B = x A C
3 2 1 mprg x A B = x A C