Metamath Proof Explorer

Theorem 2reu7

Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 . (Contributed by Alexander van der Vekens, 2-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x B
2 nfre1 ⊢ Ⅎ x ∃ x ∈ A φ
3 1 2 nfreuw ⊢ Ⅎ x ∃! y ∈ B ∃ x ∈ A φ
4 3 reuan ⊢ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! y ∈ B ∃ x ∈ A φ ∧ ∃! x ∈ A ∃ y ∈ B φ
5 ancom ⊢ ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃ y ∈ B φ ∧ ∃ x ∈ A φ
6 5 reubii ⊢ ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! y ∈ B ∃ y ∈ B φ ∧ ∃ x ∈ A φ
7 nfre1 ⊢ Ⅎ y ∃ y ∈ B φ
8 7 reuan ⊢ ∃! y ∈ B ∃ y ∈ B φ ∧ ∃ x ∈ A φ ↔ ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ
9 ancom ⊢ ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ
10 6 8 9 3bitri ⊢ ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ
11 10 reubii ⊢ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ ↔ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ
12 ancom ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃! y ∈ B ∃ x ∈ A φ ∧ ∃! x ∈ A ∃ y ∈ B φ
13 4 11 12 3bitr4ri ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃! x ∈ A ∃! y ∈ B ∃ x ∈ A φ ∧ ∃ y ∈ B φ