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

Metamath Proof Explorer

Theorem r3ex

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

Ref Expression
Assertion r3ex ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 r2ex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐶 𝜑 ) )
2 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐶 𝜑 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) )
3 2 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐶 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) )
4 19.42v ⊢ ( ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) )
5 anass ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) )
6 5 bicomi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )
7 df-3an ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) )
8 7 bicomi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
9 6 8 bianbi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )
10 9 exbii ⊢ ( ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝜑 ) ) ↔ ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )
11 3 4 10 3bitr2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐶 𝜑 ) ↔ ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )
12 11 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐶 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )
13 1 12 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝜑 ) )