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 
|- ( 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 )