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

Metamath Proof Explorer

Theorem eluni2f

Description: Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses eluni2f.1 ⊢ Ⅎ _ x A
eluni2f.2 ⊢ Ⅎ _ x B
Assertion eluni2f ⊢ A ∈ ⋃ B ↔ ∃ x ∈ B A ∈ x

Proof

Step Hyp Ref Expression
1 eluni2f.1 ⊢ Ⅎ _ x A
2 eluni2f.2 ⊢ Ⅎ _ x B
3 exancom ⊢ ∃ x A ∈ x ∧ x ∈ B ↔ ∃ x x ∈ B ∧ A ∈ x
4 1 2 elunif ⊢ A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B
5 df-rex ⊢ ∃ x ∈ B A ∈ x ↔ ∃ x x ∈ B ∧ A ∈ x
6 3 4 5 3bitr4i ⊢ A ∈ ⋃ B ↔ ∃ x ∈ B A ∈ x