Theorem iuneq12i

Description: Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	iuneq12i.1	⊢ 𝐴 = 𝐵
	iuneq12i.2	⊢ 𝐶 = 𝐷
Assertion	iuneq12i	⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷

Proof

Step	Hyp	Ref	Expression
1		iuneq12i.1	⊢ 𝐴 = 𝐵
2		iuneq12i.2	⊢ 𝐶 = 𝐷
3	2	eleq2i	⊢ ( 𝑡 ∈ 𝐶 ↔ 𝑡 ∈ 𝐷 )
4	1 3	rexeqbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑡 ∈ 𝐷 )
5	4	abbii	⊢ { 𝑡 ∣ ∃ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 } = { 𝑡 ∣ ∃ 𝑥 ∈ 𝐵 𝑡 ∈ 𝐷 }
6		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = { 𝑡 ∣ ∃ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 }
7		df-iun	⊢ ∪ 𝑥 ∈ 𝐵 𝐷 = { 𝑡 ∣ ∃ 𝑥 ∈ 𝐵 𝑡 ∈ 𝐷 }
8	5 6 7	3eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷