Metamath Proof Explorer

Theorem ralxp3es

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

Ref Expression
Assertion ralxp3es 
|- ( A. x e. ( ( A X. B ) X. C ) [. ( 1st ` ( 1st ` x ) ) / y ]. [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph <-> A. y e. A A. z e. B A. w e. C ph )

Proof

Step Hyp Ref Expression
1 nfsbc1v 
 |-  F/ y [. ( 1st ` ( 1st ` x ) ) / y ]. [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph
2 nfcv 
 |-  F/_ z ( 1st ` ( 1st ` x ) )
3 nfsbc1v 
 |-  F/ z [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph
4 2 3 nfsbcw 
 |-  F/ z [. ( 1st ` ( 1st ` x ) ) / y ]. [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph
5 nfcv 
 |-  F/_ w ( 1st ` ( 1st ` x ) )
6 nfcv 
 |-  F/_ w ( 2nd ` ( 1st ` x ) )
7 nfsbc1v 
 |-  F/ w [. ( 2nd ` x ) / w ]. ph
8 6 7 nfsbcw 
 |-  F/ w [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph
9 5 8 nfsbcw 
 |-  F/ w [. ( 1st ` ( 1st ` x ) ) / y ]. [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph
10 nfv 
 |-  F/ x ph
11 sbcoteq1a 
 |-  ( x = <. <. y , z >. , w >. -> ( [. ( 1st ` ( 1st ` x ) ) / y ]. [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph <-> ph ) )
12 1 4 9 10 11 ralxp3f 
 |-  ( A. x e. ( ( A X. B ) X. C ) [. ( 1st ` ( 1st ` x ) ) / y ]. [. ( 2nd ` ( 1st ` x ) ) / z ]. [. ( 2nd ` x ) / w ]. ph <-> A. y e. A A. z e. B A. w e. C ph )