Theorem elunii

Description: Membership in class union. (Contributed by NM, 24-Mar-1995)

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

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )
2		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
3	1 2	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) ) )
4	3	spcegv	⊢ ( 𝐵 ∈ 𝐶 → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶 ) ) )
5	4	anabsi7	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶 ) )
6		eluni	⊢ ( 𝐴 ∈ ∪ 𝐶 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶 ) )
7	5 6	sylibr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ ∪ 𝐶 )