Metamath Proof Explorer


Theorem iuneq2i

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

Ref Expression
Hypothesis iuneq2i.1 ( 𝑥𝐴𝐵 = 𝐶 )
Assertion iuneq2i 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶

Proof

Step Hyp Ref Expression
1 iuneq2i.1 ( 𝑥𝐴𝐵 = 𝐶 )
2 iuneq2 ( ∀ 𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 )
3 2 1 mprg 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶