Theorem eliunid

Description: Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Assertion	eliunid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rspe	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
2		eliun	⊢ ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
3	1 2	sylibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )