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 \left(\left(A\times B\right)\times C\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(x\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(x\right)\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(x\right)/w\underset{\dot{}}{]}\phi \leftrightarrow \forall y\in A\forall z\in B\forall w\in C\phi$$

Proof

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