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

Metamath Proof Explorer

Theorem 2rexreu

Description: Double restricted existential uniqueness implies double restricted unique existential quantification, analogous to 2exeu . (Contributed by Alexander van der Vekens, 25-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 reurmo ⊢ ∃! x ∈ A ∃ y ∈ B φ → ∃* x ∈ A ∃ y ∈ B φ
2 reurex ⊢ ∃! y ∈ B φ → ∃ y ∈ B φ
3 2 rmoimi ⊢ ∃* x ∈ A ∃ y ∈ B φ → ∃* x ∈ A ∃! y ∈ B φ
4 1 3 syl ⊢ ∃! x ∈ A ∃ y ∈ B φ → ∃* x ∈ A ∃! y ∈ B φ
5 2reurex ⊢ ∃! y ∈ B ∃ x ∈ A φ → ∃ x ∈ A ∃! y ∈ B φ
6 4 5 anim12ci ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ → ∃ x ∈ A ∃! y ∈ B φ ∧ ∃* x ∈ A ∃! y ∈ B φ
7 reu5 ⊢ ∃! x ∈ A ∃! y ∈ B φ ↔ ∃ x ∈ A ∃! y ∈ B φ ∧ ∃* x ∈ A ∃! y ∈ B φ
8 6 7 sylibr ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ → ∃! x ∈ A ∃! y ∈ B φ