Metamath Proof Explorer


Theorem iuneq2df

Description: Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses iuneq2df.1 𝑥 𝜑
iuneq2df.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 = 𝐶 )
Assertion iuneq2df ( 𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 iuneq2df.1 𝑥 𝜑
2 iuneq2df.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 = 𝐶 )
3 2 ex ( 𝜑 → ( 𝑥𝐴𝐵 = 𝐶 ) )
4 1 3 ralrimi ( 𝜑 → ∀ 𝑥𝐴 𝐵 = 𝐶 )
5 iuneq2 ( ∀ 𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 )
6 4 5 syl ( 𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 )