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

Metamath Proof Explorer

Theorem elunif

Description: A version of eluni using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 elunif.1 ⊢ Ⅎ _ x A
2 elunif.2 ⊢ Ⅎ _ x B
3 eluni ⊢ A ∈ ⋃ B ↔ ∃ y A ∈ y ∧ y ∈ B
4 nfcv ⊢ Ⅎ _ x y
5 1 4 nfel ⊢ Ⅎ x A ∈ y
6 4 2 nfel ⊢ Ⅎ x y ∈ B
7 5 6 nfan ⊢ Ⅎ x A ∈ y ∧ y ∈ B
8 nfv ⊢ Ⅎ y A ∈ x ∧ x ∈ B
9 eleq2w ⊢ y = x → A ∈ y ↔ A ∈ x
10 eleq1w ⊢ y = x → y ∈ B ↔ x ∈ B
11 9 10 anbi12d ⊢ y = x → A ∈ y ∧ y ∈ B ↔ A ∈ x ∧ x ∈ B
12 7 8 11 cbvexv1 ⊢ ∃ y A ∈ y ∧ y ∈ B ↔ ∃ x A ∈ x ∧ x ∈ B
13 3 12 bitri ⊢ A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B