Metamath Proof Explorer

Theorem iuneq2d

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

Ref Expression
Hypothesis iuneq2d.2 
|- ( ph -> B = C )
Assertion iuneq2d 
|- ( ph -> U_ x e. A B = U_ x e. A C )

Proof

Step Hyp Ref Expression
1 iuneq2d.2 
 |-  ( ph -> B = C )
2 1 adantr 
 |-  ( ( ph /\ x e. A ) -> B = C )
3 2 iuneq2dv 
 |-  ( ph -> U_ x e. A B = U_ x e. A C )