This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )