Metamath Proof Explorer

Theorem 2rexrsb

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

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

Proof

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