Theorem ralxp3f

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

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

Proof

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