ralxpes

Description: A version of ralxp with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024)

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

Step	Hyp	Ref	Expression
1		nfsbc1v	⊢ Ⅎ 𝑦 [ ( 1^st ‘ 𝑥 ) / 𝑦 ] [ ( 2^nd ‘ 𝑥 ) / 𝑧 ] 𝜑
2		nfcv	⊢ Ⅎ 𝑧 ( 1^st ‘ 𝑥 )
3		nfsbc1v	⊢ Ⅎ 𝑧 [ ( 2^nd ‘ 𝑥 ) / 𝑧 ] 𝜑
4	2 3	nfsbcw	⊢ Ⅎ 𝑧 [ ( 1^st ‘ 𝑥 ) / 𝑦 ] [ ( 2^nd ‘ 𝑥 ) / 𝑧 ] 𝜑
5		nfv	⊢ Ⅎ 𝑥 𝜑
6		sbcopeq1a	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( [ ( 1^st ‘ 𝑥 ) / 𝑦 ] [ ( 2^nd ‘ 𝑥 ) / 𝑧 ] 𝜑 ↔ 𝜑 ) )
7	1 4 5 6	ralxpf	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) [ ( 1^st ‘ 𝑥 ) / 𝑦 ] [ ( 2^nd ‘ 𝑥 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜑 )

Metamath Proof Explorer