Metamath Proof Explorer

Theorem 2ex2rexrot

Description: Rotate two existential quantifiers and two restricted existential quantifiers. (Contributed by AV, 9-Nov-2023)

Ref Expression
Assertion 2ex2rexrot ⊢ ∃ x ∃ y ∃ z ∈ A ∃ w ∈ B φ ↔ ∃ z ∈ A ∃ w ∈ B ∃ x ∃ y φ

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ∃ w ∈ B ∃ x ∃ y φ ↔ ∃ x ∃ w ∈ B ∃ y φ
2 1 rexbii ⊢ ∃ z ∈ A ∃ w ∈ B ∃ x ∃ y φ ↔ ∃ z ∈ A ∃ x ∃ w ∈ B ∃ y φ
3 rexcom4 ⊢ ∃ z ∈ A ∃ x ∃ w ∈ B ∃ y φ ↔ ∃ x ∃ z ∈ A ∃ w ∈ B ∃ y φ
4 rexcom4 ⊢ ∃ w ∈ B ∃ y φ ↔ ∃ y ∃ w ∈ B φ
5 4 rexbii ⊢ ∃ z ∈ A ∃ w ∈ B ∃ y φ ↔ ∃ z ∈ A ∃ y ∃ w ∈ B φ
6 rexcom4 ⊢ ∃ z ∈ A ∃ y ∃ w ∈ B φ ↔ ∃ y ∃ z ∈ A ∃ w ∈ B φ
7 5 6 bitri ⊢ ∃ z ∈ A ∃ w ∈ B ∃ y φ ↔ ∃ y ∃ z ∈ A ∃ w ∈ B φ
8 7 exbii ⊢ ∃ x ∃ z ∈ A ∃ w ∈ B ∃ y φ ↔ ∃ x ∃ y ∃ z ∈ A ∃ w ∈ B φ
9 2 3 8 3bitrri ⊢ ∃ x ∃ y ∃ z ∈ A ∃ w ∈ B φ ↔ ∃ z ∈ A ∃ w ∈ B ∃ x ∃ y φ