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

Metamath Proof Explorer

Theorem 2reu4

Description: Definition of double restricted existential uniqueness ("exactly one x and exactly one y "), analogous to 2eu4 . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion 2reu4 ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃ x ∈ A ∃ y ∈ B φ ∧ ∃ z ∈ A ∃ w ∈ B ∀ x ∈ A ∀ y ∈ B φ → x = z ∧ y = w

Proof

Step Hyp Ref Expression
1 reurex ⊢ ∃! x ∈ A ∃ y ∈ B φ → ∃ x ∈ A ∃ y ∈ B φ
2 rexn0 ⊢ ∃ x ∈ A ∃ y ∈ B φ → A ≠ ∅
3 1 2 syl ⊢ ∃! x ∈ A ∃ y ∈ B φ → A ≠ ∅
4 reurex ⊢ ∃! y ∈ B ∃ x ∈ A φ → ∃ y ∈ B ∃ x ∈ A φ
5 rexn0 ⊢ ∃ y ∈ B ∃ x ∈ A φ → B ≠ ∅
6 4 5 syl ⊢ ∃! y ∈ B ∃ x ∈ A φ → B ≠ ∅
7 3 6 anim12i ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ → A ≠ ∅ ∧ B ≠ ∅
8 ne0i ⊢ x ∈ A → A ≠ ∅
9 ne0i ⊢ y ∈ B → B ≠ ∅
10 8 9 anim12i ⊢ x ∈ A ∧ y ∈ B → A ≠ ∅ ∧ B ≠ ∅
11 10 a1d ⊢ x ∈ A ∧ y ∈ B → φ → A ≠ ∅ ∧ B ≠ ∅
12 11 rexlimivv ⊢ ∃ x ∈ A ∃ y ∈ B φ → A ≠ ∅ ∧ B ≠ ∅
13 12 adantr ⊢ ∃ x ∈ A ∃ y ∈ B φ ∧ ∃ z ∈ A ∃ w ∈ B ∀ x ∈ A ∀ y ∈ B φ → x = z ∧ y = w → A ≠ ∅ ∧ B ≠ ∅
14 2reu4lem ⊢ A ≠ ∅ ∧ B ≠ ∅ → ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃ x ∈ A ∃ y ∈ B φ ∧ ∃ z ∈ A ∃ w ∈ B ∀ x ∈ A ∀ y ∈ B φ → x = z ∧ y = w
15 7 13 14 pm5.21nii ⊢ ∃! x ∈ A ∃ y ∈ B φ ∧ ∃! y ∈ B ∃ x ∈ A φ ↔ ∃ x ∈ A ∃ y ∈ B φ ∧ ∃ z ∈ A ∃ w ∈ B ∀ x ∈ A ∀ y ∈ B φ → x = z ∧ y = w