Theorem eluni

Description: Membership in class union. (Contributed by NM, 22-May-1994)

	Ref	Expression
Assertion	eluni	⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V )
2		elex	⊢ ( 𝐴 ∈ 𝑥 → 𝐴 ∈ V )
3	2	adantr	⊢ ( ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ V )
4	3	exlimiv	⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ V )
5		elequ1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
6	5	anbi1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
7	6	exbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
8		eleq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
9	8	anbi1d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
10	9	exbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
11		df-uni	⊢ ∪ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) }
12	7 10 11	elab2gw	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
13	1 4 12	pm5.21nii	⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )