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	$⊢ \exists x \in A \exists y \in B \exists z \in C φ \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land φ)$

Proof

Step	Hyp	Ref	Expression
1		r2ex	$⊢ \exists x \in A \exists y \in B \exists z \in C φ \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land \exists z \in C φ)$
2		df-rex	$⊢ \exists z \in C φ \leftrightarrow \exists z (z \in C \land φ)$
3	2	anbi2i	$⊢ ((x \in A \land y \in B) \land \exists z \in C φ) \leftrightarrow ((x \in A \land y \in B) \land \exists z (z \in C \land φ))$
4		19.42v	$⊢ \exists z ((x \in A \land y \in B) \land (z \in C \land φ)) \leftrightarrow ((x \in A \land y \in B) \land \exists z (z \in C \land φ))$
5		anass	$⊢ (((x \in A \land y \in B) \land z \in C) \land φ) \leftrightarrow ((x \in A \land y \in B) \land (z \in C \land φ))$
6	5	bicomi	$⊢ ((x \in A \land y \in B) \land (z \in C \land φ)) \leftrightarrow (((x \in A \land y \in B) \land z \in C) \land φ)$
7		df-3an	$⊢ (x \in A \land y \in B \land z \in C) \leftrightarrow ((x \in A \land y \in B) \land z \in C)$
8	7	bicomi	$⊢ ((x \in A \land y \in B) \land z \in C) \leftrightarrow (x \in A \land y \in B \land z \in C)$
9	6 8	bianbi	$⊢ ((x \in A \land y \in B) \land (z \in C \land φ)) \leftrightarrow ((x \in A \land y \in B \land z \in C) \land φ)$
10	9	exbii	$⊢ \exists z ((x \in A \land y \in B) \land (z \in C \land φ)) \leftrightarrow \exists z ((x \in A \land y \in B \land z \in C) \land φ)$
11	3 4 10	3bitr2i	$⊢ ((x \in A \land y \in B) \land \exists z \in C φ) \leftrightarrow \exists z ((x \in A \land y \in B \land z \in C) \land φ)$
12	11	2exbii	$⊢ \exists x \exists y ((x \in A \land y \in B) \land \exists z \in C φ) \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land φ)$
13	1 12	bitri	$⊢ \exists x \in A \exists y \in B \exists z \in C φ \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land φ)$