Metamath Proof Explorer


Theorem ralxpes

Description: A version of ralxp with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Assertion ralxpes x A × B [˙ 1 st x / y]˙ [˙ 2 nd x / z]˙ φ y A z B φ

Proof

Step Hyp Ref Expression
1 nfsbc1v y [˙ 1 st x / y]˙ [˙ 2 nd x / z]˙ φ
2 nfcv _ z 1 st x
3 nfsbc1v z [˙ 2 nd x / z]˙ φ
4 2 3 nfsbcw z [˙ 1 st x / y]˙ [˙ 2 nd x / z]˙ φ
5 nfv x φ
6 sbcopeq1a x = y z [˙ 1 st x / y]˙ [˙ 2 nd x / z]˙ φ φ
7 1 4 5 6 ralxpf x A × B [˙ 1 st x / y]˙ [˙ 2 nd x / z]˙ φ y A z B φ