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	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )