Metamath Proof Explorer


Theorem iuneq1i

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

Ref Expression
Hypothesis iuneq1i.1 𝐴 = 𝐵
Assertion iuneq1i 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶

Proof

Step Hyp Ref Expression
1 iuneq1i.1 𝐴 = 𝐵
2 iuneq1 ( 𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 )
3 1 2 ax-mp 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶