This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iuneqconst

Description: Indexed union of identical classes. (Contributed by AV, 5-Mar-2024)

Ref Expression
Hypothesis iuneqconst.p ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
Assertion iuneqconst ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 iuneqconst.p ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
2 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
3 1 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) )
4 3 rspcev ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5 4 adantlr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
6 5 ex ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ( 𝑦 ∈ 𝐶 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
7 nfv ⊢ Ⅎ 𝑥 𝑋 ∈ 𝐴
8 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶
9 7 8 nfan ⊢ Ⅎ 𝑥 ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )
10 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐶
11 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ( 𝑥 ∈ 𝐴 → 𝐵 = 𝐶 ) )
12 eleq2 ⊢ ( 𝐵 = 𝐶 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) )
13 12 biimpd ⊢ ( 𝐵 = 𝐶 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
14 11 13 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ) )
15 14 adantl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ) )
16 9 10 15 rexlimd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
17 6 16 impbid ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ( 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
18 2 17 bitr4id ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ 𝐶 ) )
19 18 eqrdv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )