Metamath Proof Explorer


Theorem iuneq2d

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

Ref Expression
Hypothesis iuneq2d.2 φ B = C
Assertion iuneq2d φ x A B = x A C

Proof

Step Hyp Ref Expression
1 iuneq2d.2 φ B = C
2 1 adantr φ x A B = C
3 2 iuneq2dv φ x A B = x A C