Metamath Proof Explorer

Theorem 2rexsb

Description: An equivalent expression for double restricted existence, analogous to rexsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 rexsb ⊢ ∃ y ∈ B φ ↔ ∃ w ∈ B ∀ y y = w → φ
2 1 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ x ∈ A ∃ w ∈ B ∀ y y = w → φ
3 rexcom ⊢ ∃ x ∈ A ∃ w ∈ B ∀ y y = w → φ ↔ ∃ w ∈ B ∃ x ∈ A ∀ y y = w → φ
4 2 3 bitri ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ w ∈ B ∃ x ∈ A ∀ y y = w → φ
5 rexsb ⊢ ∃ x ∈ A ∀ y y = w → φ ↔ ∃ z ∈ A ∀ x x = z → ∀ y y = w → φ
6 impexp ⊢ x = z ∧ y = w → φ ↔ x = z → y = w → φ
7 6 albii ⊢ ∀ y x = z ∧ y = w → φ ↔ ∀ y x = z → y = w → φ
8 19.21v ⊢ ∀ y x = z → y = w → φ ↔ x = z → ∀ y y = w → φ
9 7 8 bitr2i ⊢ x = z → ∀ y y = w → φ ↔ ∀ y x = z ∧ y = w → φ
10 9 albii ⊢ ∀ x x = z → ∀ y y = w → φ ↔ ∀ x ∀ y x = z ∧ y = w → φ
11 10 rexbii ⊢ ∃ z ∈ A ∀ x x = z → ∀ y y = w → φ ↔ ∃ z ∈ A ∀ x ∀ y x = z ∧ y = w → φ
12 5 11 bitri ⊢ ∃ x ∈ A ∀ y y = w → φ ↔ ∃ z ∈ A ∀ x ∀ y x = z ∧ y = w → φ
13 12 rexbii ⊢ ∃ w ∈ B ∃ x ∈ A ∀ y y = w → φ ↔ ∃ w ∈ B ∃ z ∈ A ∀ x ∀ y x = z ∧ y = w → φ
14 rexcom ⊢ ∃ w ∈ B ∃ z ∈ A ∀ x ∀ y x = z ∧ y = w → φ ↔ ∃ z ∈ A ∃ w ∈ B ∀ x ∀ y x = z ∧ y = w → φ
15 13 14 bitri ⊢ ∃ w ∈ B ∃ x ∈ A ∀ y y = w → φ ↔ ∃ z ∈ A ∃ w ∈ B ∀ x ∀ y x = z ∧ y = w → φ
16 4 15 bitri ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ z ∈ A ∃ w ∈ B ∀ x ∀ y x = z ∧ y = w → φ