Metamath Proof Explorer


Theorem ralxpes

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

Ref Expression
Assertion ralxpes ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) [ ( 1st𝑥 ) / 𝑦 ] [ ( 2nd𝑥 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑦𝐴𝑧𝐵 𝜑 )

Proof

Step Hyp Ref Expression
1 nfsbc1v 𝑦 [ ( 1st𝑥 ) / 𝑦 ] [ ( 2nd𝑥 ) / 𝑧 ] 𝜑
2 nfcv 𝑧 ( 1st𝑥 )
3 nfsbc1v 𝑧 [ ( 2nd𝑥 ) / 𝑧 ] 𝜑
4 2 3 nfsbcw 𝑧 [ ( 1st𝑥 ) / 𝑦 ] [ ( 2nd𝑥 ) / 𝑧 ] 𝜑
5 nfv 𝑥 𝜑
6 sbcopeq1a ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( [ ( 1st𝑥 ) / 𝑦 ] [ ( 2nd𝑥 ) / 𝑧 ] 𝜑𝜑 ) )
7 1 4 5 6 ralxpf ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) [ ( 1st𝑥 ) / 𝑦 ] [ ( 2nd𝑥 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑦𝐴𝑧𝐵 𝜑 )