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		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
6	5	anbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
7	6	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
8		df-uni	⊢ ∪ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) }
9	7 8	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
10	1 4 9	pm5.21nii	⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )