ralxpes

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

		Ref	Expression
	Assertion	ralxpes	$⊢ \forall x \in (A \times B) \underset{˙}{[} 1^{st} (x) / y \underset{˙}{]} \underset{˙}{[} 2^{nd} (x) / z \underset{˙}{]} φ \leftrightarrow \forall y \in A \forall z \in B φ$

Step	Hyp	Ref	Expression
1		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} 1^{st} (x) / y \underset{˙}{]} \underset{˙}{[} 2^{nd} (x) / z \underset{˙}{]} φ$
2		nfcv	$⊢ \underline{Ⅎ} z 1^{st} (x)$
3		nfsbc1v	$⊢ Ⅎ z \underset{˙}{[} 2^{nd} (x) / z \underset{˙}{]} φ$
4	2 3	nfsbcw	$⊢ Ⅎ z \underset{˙}{[} 1^{st} (x) / y \underset{˙}{]} \underset{˙}{[} 2^{nd} (x) / z \underset{˙}{]} φ$
5		nfv	$⊢ Ⅎ x φ$
6		sbcopeq1a	$⊢ x = ⟨y, z⟩ \to (\underset{˙}{[} 1^{st} (x) / y \underset{˙}{]} \underset{˙}{[} 2^{nd} (x) / z \underset{˙}{]} φ \leftrightarrow φ)$
7	1 4 5 6	ralxpf	$⊢ \forall x \in (A \times B) \underset{˙}{[} 1^{st} (x) / y \underset{˙}{]} \underset{˙}{[} 2^{nd} (x) / z \underset{˙}{]} φ \leftrightarrow \forall y \in A \forall z \in B φ$

Metamath Proof Explorer