Theorem eliuni

Description: Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021)

	Ref	Expression
Hypothesis	eliuni.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion	eliuni	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐸 ∈ 𝐶 ) → 𝐸 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eliuni.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2	1	eleq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐸 ∈ 𝐵 ↔ 𝐸 ∈ 𝐶 ) )
3	2	rspcev	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐸 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐷 𝐸 ∈ 𝐵 )
4		eliun	⊢ ( 𝐸 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 ↔ ∃ 𝑥 ∈ 𝐷 𝐸 ∈ 𝐵 )
5	3 4	sylibr	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐸 ∈ 𝐶 ) → 𝐸 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 )