Metamath Proof Explorer


Theorem iuneq12f

Description: Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses iuneq12f.1
|- F/_ x A
iuneq12f.2
|- F/_ x B
Assertion iuneq12f
|- ( ( A = B /\ A. x e. A C = D ) -> U_ x e. A C = U_ x e. B D )

Proof

Step Hyp Ref Expression
1 iuneq12f.1
 |-  F/_ x A
2 iuneq12f.2
 |-  F/_ x B
3 iuneq2
 |-  ( A. x e. A C = D -> U_ x e. A C = U_ x e. A D )
4 1 2 iuneq2f
 |-  ( A = B -> U_ x e. A D = U_ x e. B D )
5 3 4 sylan9eqr
 |-  ( ( A = B /\ A. x e. A C = D ) -> U_ x e. A C = U_ x e. B D )