Metamath Proof Explorer


Theorem iuneq1d

Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015)

Ref Expression
Hypothesis iuneq1d.1 φ A = B
Assertion iuneq1d φ x A C = x B C

Proof

Step Hyp Ref Expression
1 iuneq1d.1 φ A = B
2 iuneq1 A = B x A C = x B C
3 1 2 syl φ x A C = x B C