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

Metamath Proof Explorer

Theorem rexcom13

Description: Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015)

Ref Expression
Assertion rexcom13 ⊢ ∃ x ∈ A ∃ y ∈ B ∃ z ∈ C φ ↔ ∃ z ∈ C ∃ y ∈ B ∃ x ∈ A φ

Proof

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