Metamath Proof Explorer

Theorem 2reu8

Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 . Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E! x e. A E! y e. B using 2reu7 . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Assertion 2reu8 ⊢ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! x ∈ A ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ

Proof

Step Hyp Ref Expression
1 2reu2 ⊢ ∃! x ∈ A ∃ y ∈ B φ → ∃! y ∈ B ∃! x ∈ A φ ↔ ∃! y ∈ B ∃ x ∈ A φ
2 1 pm5.32i ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃! x ∈ A φ ↔ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ
3 nfcv ⊢ Ⅎ _ x B
4 nfreu1 ⊢ Ⅎ x ∃! x ∈ A φ
5 3 4 nfreuw ⊢ Ⅎ x ∃! y ∈ B ∃! x ∈ A φ
6 5 reuan ⊢ ∃! x ∈ A ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! y ∈ B ∃! x ∈ A φ ∧ ∃! x ∈ A ∃ y ∈ B φ
7 ancom ⊢ ∃! x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃ y ∈ B φ ∧ ∃! x ∈ A φ
8 7 reubii ⊢ ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! y ∈ B ∃ y ∈ B φ ∧ ∃! x ∈ A φ
9 nfre1 ⊢ Ⅎ y ∃ y ∈ B φ
10 9 reuan ⊢ ∃! y ∈ B ∃ y ∈ B φ ∧ ∃! x ∈ A φ ↔ ∃ y ∈ B φ ∧ ∃! y ∈ B ∃! x ∈ A φ
11 ancom ⊢ ∃ y ∈ B φ ∧ ∃! y ∈ B ∃! x ∈ A φ ↔ ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ
12 8 10 11 3bitri ⊢ ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ
13 12 reubii ⊢ ∃! x ∈ A ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! x ∈ A ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ
14 ancom ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃! x ∈ A φ ↔ ∃! y ∈ B ∃! x ∈ A φ ∧ ∃! x ∈ A ∃ y ∈ B φ
15 6 13 14 3bitr4ri ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃! x ∈ A φ ↔ ∃! x ∈ A ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ
16 2reu7 ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ
17 2 15 16 3bitr3ri ⊢ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! x ∈ A ∃! y ∈ B ∃! x ∈ A φ ∧ ∃ y ∈ B φ