Metamath Proof Explorer


Theorem iuneq2f

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

Ref Expression
Hypotheses iuneq2f.1 _ x A
iuneq2f.2 _ x B
Assertion iuneq2f A = B x A C = x B C

Proof

Step Hyp Ref Expression
1 iuneq2f.1 _ x A
2 iuneq2f.2 _ x B
3 1 2 nfeq x A = B
4 id A = B A = B
5 eqidd A = B C = C
6 3 1 2 4 5 iuneq12df A = B x A C = x B C