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 x A × B × C [˙ 1 st 1 st x / y]˙ [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ y A z B w C φ

Proof

Step Hyp Ref Expression
1 nfsbc1v y [˙ 1 st 1 st x / y]˙ [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ
2 nfcv _ z 1 st 1 st x
3 nfsbc1v z [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ
4 2 3 nfsbcw z [˙ 1 st 1 st x / y]˙ [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ
5 nfcv _ w 1 st 1 st x
6 nfcv _ w 2 nd 1 st x
7 nfsbc1v w [˙ 2 nd x / w]˙ φ
8 6 7 nfsbcw w [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ
9 5 8 nfsbcw w [˙ 1 st 1 st x / y]˙ [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ
10 nfv x φ
11 sbcoteq1a x = y z w [˙ 1 st 1 st x / y]˙ [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ φ
12 1 4 9 10 11 ralxp3f x A × B × C [˙ 1 st 1 st x / y]˙ [˙ 2 nd 1 st x / z]˙ [˙ 2 nd x / w]˙ φ y A z B w C φ