Metamath Proof Explorer


Theorem iuneq1i

Description: Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 iuneq1i.1 A = B
2 iuneq1 A = B x A C = x B C
3 1 2 ax-mp x A C = x B C