ralxp3es

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

		Ref	Expression
	Assertion	ralxp3es	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) [ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) / 𝑦 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜑 )

Step	Hyp	Ref	Expression
1		nfsbc1v	⊢ Ⅎ 𝑦 [ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) / 𝑦 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑
2		nfcv	⊢ Ⅎ 𝑧 ( 1^st ‘ ( 1^st ‘ 𝑥 ) )
3		nfsbc1v	⊢ Ⅎ 𝑧 [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑
4	2 3	nfsbcw	⊢ Ⅎ 𝑧 [ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) / 𝑦 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑
5		nfcv	⊢ Ⅎ 𝑤 ( 1^st ‘ ( 1^st ‘ 𝑥 ) )
6		nfcv	⊢ Ⅎ 𝑤 ( 2^nd ‘ ( 1^st ‘ 𝑥 ) )
7		nfsbc1v	⊢ Ⅎ 𝑤 [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑
8	6 7	nfsbcw	⊢ Ⅎ 𝑤 [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑
9	5 8	nfsbcw	⊢ Ⅎ 𝑤 [ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) / 𝑦 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑
10		nfv	⊢ Ⅎ 𝑥 𝜑
11		sbcoteq1a	⊢ ( 𝑥 = ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑤 ⟩ → ( [ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) / 𝑦 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑 ↔ 𝜑 ) )
12	1 4 9 10 11	ralxp3f	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) [ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) / 𝑦 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) / 𝑧 ] [ ( 2^nd ‘ 𝑥 ) / 𝑤 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜑 )

Metamath Proof Explorer