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

Metamath Proof Explorer

Theorem rexrot4

Description: Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015)

Ref Expression
Assertion rexrot4 ⊢ ∃ x ∈ A ∃ y ∈ B ∃ z ∈ C ∃ w ∈ D φ ↔ ∃ z ∈ C ∃ w ∈ D ∃ x ∈ A ∃ y ∈ B φ

Proof

Step Hyp Ref Expression
1 rexcom13 ⊢ ∃ y ∈ B ∃ z ∈ C ∃ w ∈ D φ ↔ ∃ w ∈ D ∃ z ∈ C ∃ y ∈ B φ
2 1 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B ∃ z ∈ C ∃ w ∈ D φ ↔ ∃ x ∈ A ∃ w ∈ D ∃ z ∈ C ∃ y ∈ B φ
3 rexcom13 ⊢ ∃ x ∈ A ∃ w ∈ D ∃ z ∈ C ∃ y ∈ B φ ↔ ∃ z ∈ C ∃ w ∈ D ∃ x ∈ A ∃ y ∈ B φ
4 2 3 bitri ⊢ ∃ x ∈ A ∃ y ∈ B ∃ z ∈ C ∃ w ∈ D φ ↔ ∃ z ∈ C ∃ w ∈ D ∃ x ∈ A ∃ y ∈ B φ