ralxp3f

Description: Restricted for all over a triple cross product. (Contributed by Scott Fenton, 22-Aug-2024)

	Ref	Expression
Hypotheses	ral3xpf.1	$⊢ Ⅎ y φ$
	ral3xpf.2	$⊢ Ⅎ z φ$
	ral3xpf.3	$⊢ Ⅎ w φ$
	ral3xpf.4	$⊢ Ⅎ x ψ$
	ral3xpf.5	$⊢ x = ⟨⟨y, z⟩, w⟩ \to (φ \leftrightarrow ψ)$
Assertion	ralxp3f	$⊢ \forall x \in ((A \times B) \times C) φ \leftrightarrow \forall y \in A \forall z \in B \forall w \in C ψ$

Proof

Step	Hyp	Ref	Expression
1		ral3xpf.1	$⊢ Ⅎ y φ$
2		ral3xpf.2	$⊢ Ⅎ z φ$
3		ral3xpf.3	$⊢ Ⅎ w φ$
4		ral3xpf.4	$⊢ Ⅎ x ψ$
5		ral3xpf.5	$⊢ x = ⟨⟨y, z⟩, w⟩ \to (φ \leftrightarrow ψ)$
6		df-ral	$⊢ \forall x \in ((A \times B) \times C) φ \leftrightarrow \forall x (x \in ((A \times B) \times C) \to φ)$
7	1	r19.23	$⊢ \forall y \in A (\exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow (\exists y \in A \exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
8	3	r19.23	$⊢ \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow (\exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
9	8	ralbii	$⊢ \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall z \in B (\exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
10	2	r19.23	$⊢ \forall z \in B (\exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow (\exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
11	9 10	bitri	$⊢ \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow (\exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
12	11	ralbii	$⊢ \forall y \in A \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall y \in A (\exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
13		elxpxp	$⊢ x \in ((A \times B) \times C) \leftrightarrow \exists y \in A \exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩$
14	13	imbi1i	$⊢ (x \in ((A \times B) \times C) \to φ) \leftrightarrow (\exists y \in A \exists z \in B \exists w \in C x = ⟨⟨y, z⟩, w⟩ \to φ)$
15	7 12 14	3bitr4ri	$⊢ (x \in ((A \times B) \times C) \to φ) \leftrightarrow \forall y \in A \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ)$
16	15	albii	$⊢ \forall x (x \in ((A \times B) \times C) \to φ) \leftrightarrow \forall x \forall y \in A \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ)$
17		ralcom4	$⊢ \forall y \in A \forall x \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall x \forall y \in A \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ)$
18		ralcom4	$⊢ \forall z \in B \forall x \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall x \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ)$
19		ralcom4	$⊢ \forall w \in C \forall x (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall x \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ)$
20		opex	$⊢ ⟨⟨y, z⟩, w⟩ \in V$
21	4 20 5	ceqsal	$⊢ \forall x (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow ψ$
22	21	ralbii	$⊢ \forall w \in C \forall x (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall w \in C ψ$
23	19 22	bitr3i	$⊢ \forall x \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall w \in C ψ$
24	23	ralbii	$⊢ \forall z \in B \forall x \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall z \in B \forall w \in C ψ$
25	18 24	bitr3i	$⊢ \forall x \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall z \in B \forall w \in C ψ$
26	25	ralbii	$⊢ \forall y \in A \forall x \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall y \in A \forall z \in B \forall w \in C ψ$
27	17 26	bitr3i	$⊢ \forall x \forall y \in A \forall z \in B \forall w \in C (x = ⟨⟨y, z⟩, w⟩ \to φ) \leftrightarrow \forall y \in A \forall z \in B \forall w \in C ψ$
28	6 16 27	3bitri	$⊢ \forall x \in ((A \times B) \times C) φ \leftrightarrow \forall y \in A \forall z \in B \forall w \in C ψ$

Metamath Proof Explorer

Theorem ralxp3f

Proof