Metamath Proof Explorer

Theorem ralxpes

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

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

Proof

Step Hyp Ref Expression
1 nfsbc1v 
 |-  F/ y [. ( 1st ` x ) / y ]. [. ( 2nd ` x ) / z ]. ph
2 nfcv 
 |-  F/_ z ( 1st ` x )
3 nfsbc1v 
 |-  F/ z [. ( 2nd ` x ) / z ]. ph
4 2 3 nfsbcw 
 |-  F/ z [. ( 1st ` x ) / y ]. [. ( 2nd ` x ) / z ]. ph
5 nfv 
 |-  F/ x ph
6 sbcopeq1a 
 |-  ( x = <. y , z >. -> ( [. ( 1st ` x ) / y ]. [. ( 2nd ` x ) / z ]. ph <-> ph ) )
7 1 4 5 6 ralxpf 
 |-  ( A. x e. ( A X. B ) [. ( 1st ` x ) / y ]. [. ( 2nd ` x ) / z ]. ph <-> A. y e. A A. z e. B ph )