This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralxp3es

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

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

Proof

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