Metamath Proof Explorer

Theorem r3ex

Description: Triple existential quantification. (Contributed by AV, 21-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 r2ex ⊢ ∃ x ∈ A ∃ y ∈ B ∃ z ∈ C φ ↔ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ ∃ z ∈ C φ
2 df-rex ⊢ ∃ z ∈ C φ ↔ ∃ z z ∈ C ∧ φ
3 2 anbi2i ⊢ x ∈ A ∧ y ∈ B ∧ ∃ z ∈ C φ ↔ x ∈ A ∧ y ∈ B ∧ ∃ z z ∈ C ∧ φ
4 19.42v ⊢ ∃ z x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ ↔ x ∈ A ∧ y ∈ B ∧ ∃ z z ∈ C ∧ φ
5 anass ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ
6 5 bicomi ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ
7 df-3an ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C
8 7 bicomi ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C
9 6 8 bianbi ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ
10 9 exbii ⊢ ∃ z x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ ↔ ∃ z x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ
11 3 4 10 3bitr2i ⊢ x ∈ A ∧ y ∈ B ∧ ∃ z ∈ C φ ↔ ∃ z x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ
12 11 2exbii ⊢ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ ∃ z ∈ C φ ↔ ∃ x ∃ y ∃ z x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ
13 1 12 bitri ⊢ ∃ x ∈ A ∃ y ∈ B ∃ z ∈ C φ ↔ ∃ x ∃ y ∃ z x ∈ A ∧ y ∈ B ∧ z ∈ C ∧ φ