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

Metamath Proof Explorer

Theorem 2reurex

Description: Double restricted quantification with existential uniqueness, analogous to 2euex . (Contributed by Alexander van der Vekens, 24-Jun-2017)

Ref Expression
Assertion 2reurex ⊢ ∃! x ∈ A ∃ y ∈ B φ → ∃ y ∈ B ∃! x ∈ A φ

Proof

Step Hyp Ref Expression
1 reu5 ⊢ ∃! x ∈ A ∃ y ∈ B φ ↔ ∃ x ∈ A ∃ y ∈ B φ ∧ ∃* x ∈ A ∃ y ∈ B φ
2 rexcom ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ y ∈ B ∃ x ∈ A φ
3 nfcv ⊢ Ⅎ _ y A
4 nfre1 ⊢ Ⅎ y ∃ y ∈ B φ
5 3 4 nfrmow ⊢ Ⅎ y ∃* x ∈ A ∃ y ∈ B φ
6 rspe ⊢ y ∈ B ∧ φ → ∃ y ∈ B φ
7 6 ex ⊢ y ∈ B → φ → ∃ y ∈ B φ
8 7 ralrimivw ⊢ y ∈ B → ∀ x ∈ A φ → ∃ y ∈ B φ
9 rmoim ⊢ ∀ x ∈ A φ → ∃ y ∈ B φ → ∃* x ∈ A ∃ y ∈ B φ → ∃* x ∈ A φ
10 8 9 syl ⊢ y ∈ B → ∃* x ∈ A ∃ y ∈ B φ → ∃* x ∈ A φ
11 10 impcom ⊢ ∃* x ∈ A ∃ y ∈ B φ ∧ y ∈ B → ∃* x ∈ A φ
12 rmo5 ⊢ ∃* x ∈ A φ ↔ ∃ x ∈ A φ → ∃! x ∈ A φ
13 11 12 sylib ⊢ ∃* x ∈ A ∃ y ∈ B φ ∧ y ∈ B → ∃ x ∈ A φ → ∃! x ∈ A φ
14 13 ex ⊢ ∃* x ∈ A ∃ y ∈ B φ → y ∈ B → ∃ x ∈ A φ → ∃! x ∈ A φ
15 5 14 reximdai ⊢ ∃* x ∈ A ∃ y ∈ B φ → ∃ y ∈ B ∃ x ∈ A φ → ∃ y ∈ B ∃! x ∈ A φ
16 2 15 biimtrid ⊢ ∃* x ∈ A ∃ y ∈ B φ → ∃ x ∈ A ∃ y ∈ B φ → ∃ y ∈ B ∃! x ∈ A φ
17 16 impcom ⊢ ∃ x ∈ A ∃ y ∈ B φ ∧ ∃* x ∈ A ∃ y ∈ B φ → ∃ y ∈ B ∃! x ∈ A φ
18 1 17 sylbi ⊢ ∃! x ∈ A ∃ y ∈ B φ → ∃ y ∈ B ∃! x ∈ A φ