Theorem ralxp3

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

	Ref	Expression
Hypothesis	ralxp3.1	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	ralxp3	⊢ ( ∀ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ralxp3.1	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2		nfv	⊢ Ⅎ 𝑥 𝜑
3		nfv	⊢ Ⅎ 𝑦 𝜑
4		nfv	⊢ Ⅎ 𝑧 𝜑
5		nfv	⊢ Ⅎ 𝑝 𝜓
6	2 3 4 5 1	ralxp3f	⊢ ( ∀ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 )