Theorem ralxp3f

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

	Ref	Expression
Hypotheses	ral3xpf.1	⊢ Ⅎ 𝑦 𝜑
	ral3xpf.2	⊢ Ⅎ 𝑧 𝜑
	ral3xpf.3	⊢ Ⅎ 𝑤 𝜑
	ral3xpf.4	⊢ Ⅎ 𝑥 𝜓
	ral3xpf.5	⊢ ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	ralxp3f	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ral3xpf.1	⊢ Ⅎ 𝑦 𝜑
2		ral3xpf.2	⊢ Ⅎ 𝑧 𝜑
3		ral3xpf.3	⊢ Ⅎ 𝑤 𝜑
4		ral3xpf.4	⊢ Ⅎ 𝑥 𝜓
5		ral3xpf.5	⊢ ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → ( 𝜑 ↔ 𝜓 ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) )
7	1	r19.23	⊢ ( ∀ 𝑦 ∈ 𝐴 ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
8	3	r19.23	⊢ ( ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
9	8	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
10	2	r19.23	⊢ ( ∀ 𝑧 ∈ 𝐵 ( ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
11	9 10	bitri	⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
12	11	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
13		elxpxp	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ )
14	13	imbi1i	⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
15	7 12 14	3bitr4ri	⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
16	15	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
17		ralcom4	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
18		ralcom4	⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
19		ralcom4	⊢ ( ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) )
20		opex	⊢ ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ ∈ V
21	4 20 5	ceqsal	⊢ ( ∀ 𝑥 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ 𝜓 )
22	21	ralbii	⊢ ( ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑤 ∈ 𝐶 𝜓 )
23	19 22	bitr3i	⊢ ( ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑤 ∈ 𝐶 𝜓 )
24	23	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
25	18 24	bitr3i	⊢ ( ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
26	25	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
27	17 26	bitr3i	⊢ ( ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
28	6 16 27	3bitri	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )