Metamath Proof Explorer


Theorem iuneq12f

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

Ref Expression
Hypotheses iuneq12f.1 𝑥 𝐴
iuneq12f.2 𝑥 𝐵
Assertion iuneq12f ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥𝐴 𝐶 = 𝐷 ) → 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 iuneq12f.1 𝑥 𝐴
2 iuneq12f.2 𝑥 𝐵
3 iuneq2 ( ∀ 𝑥𝐴 𝐶 = 𝐷 𝑥𝐴 𝐶 = 𝑥𝐴 𝐷 )
4 1 2 iuneq2f ( 𝐴 = 𝐵 𝑥𝐴 𝐷 = 𝑥𝐵 𝐷 )
5 3 4 sylan9eqr ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥𝐴 𝐶 = 𝐷 ) → 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷 )