Description: A version of ralxp with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | ralxpes | ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) [ ( 1st ‘ 𝑥 ) / 𝑦 ] [ ( 2nd ‘ 𝑥 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜑 ) |
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 ‘ 𝑥 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜑 ) |