Metamath Proof Explorer


Theorem iuneq2i

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

Ref Expression
Hypothesis iuneq2i.1
|- ( x e. A -> B = C )
Assertion iuneq2i
|- U_ x e. A B = U_ x e. A C

Proof

Step Hyp Ref Expression
1 iuneq2i.1
 |-  ( x e. A -> B = C )
2 iuneq2
 |-  ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )
3 2 1 mprg
 |-  U_ x e. A B = U_ x e. A C