# Metamath Proof Explorer

## Theorem ralxpf

Description: Version of ralxp with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses ralxpf.1 𝑦 𝜑
ralxpf.2 𝑧 𝜑
ralxpf.3 𝑥 𝜓
ralxpf.4 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑𝜓 ) )
Assertion ralxpf ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∀ 𝑦𝐴𝑧𝐵 𝜓 )

### Proof

Step Hyp Ref Expression
1 ralxpf.1 𝑦 𝜑
2 ralxpf.2 𝑧 𝜑
3 ralxpf.3 𝑥 𝜓
4 ralxpf.4 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑𝜓 ) )
5 cbvralsvw ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) [ 𝑤 / 𝑥 ] 𝜑 )
6 cbvralsvw ( ∀ 𝑧𝐵 [ 𝑢 / 𝑦 ] 𝜓 ↔ ∀ 𝑣𝐵 [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 )
7 6 ralbii ( ∀ 𝑢𝐴𝑧𝐵 [ 𝑢 / 𝑦 ] 𝜓 ↔ ∀ 𝑢𝐴𝑣𝐵 [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 )
8 nfv 𝑢𝑧𝐵 𝜓
9 nfcv 𝑦 𝐵
10 nfs1v 𝑦 [ 𝑢 / 𝑦 ] 𝜓
11 9 10 nfralw 𝑦𝑧𝐵 [ 𝑢 / 𝑦 ] 𝜓
12 sbequ12 ( 𝑦 = 𝑢 → ( 𝜓 ↔ [ 𝑢 / 𝑦 ] 𝜓 ) )
13 12 ralbidv ( 𝑦 = 𝑢 → ( ∀ 𝑧𝐵 𝜓 ↔ ∀ 𝑧𝐵 [ 𝑢 / 𝑦 ] 𝜓 ) )
14 8 11 13 cbvralw ( ∀ 𝑦𝐴𝑧𝐵 𝜓 ↔ ∀ 𝑢𝐴𝑧𝐵 [ 𝑢 / 𝑦 ] 𝜓 )
15 vex 𝑢 ∈ V
16 vex 𝑣 ∈ V
17 15 16 eqvinop ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ∃ 𝑦𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
18 1 nfsbv 𝑦 [ 𝑤 / 𝑥 ] 𝜑
19 10 nfsbv 𝑦 [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓
20 18 19 nfbi 𝑦 ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 )
21 2 nfsbv 𝑧 [ 𝑤 / 𝑥 ] 𝜑
22 nfs1v 𝑧 [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓
23 21 22 nfbi 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 )
24 3 4 sbhypf ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( [ 𝑤 / 𝑥 ] 𝜑𝜓 ) )
25 vex 𝑦 ∈ V
26 vex 𝑧 ∈ V
27 25 26 opth ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ↔ ( 𝑦 = 𝑢𝑧 = 𝑣 ) )
28 sbequ12 ( 𝑧 = 𝑣 → ( [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
29 12 28 sylan9bb ( ( 𝑦 = 𝑢𝑧 = 𝑣 ) → ( 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
30 27 29 sylbi ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
31 24 30 sylan9bb ( ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
32 23 31 exlimi ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
33 20 32 exlimi ( ∃ 𝑦𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
34 17 33 sylbi ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
35 34 ralxp ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) [ 𝑤 / 𝑥 ] 𝜑 ↔ ∀ 𝑢𝐴𝑣𝐵 [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑦 ] 𝜓 )
36 7 14 35 3bitr4ri ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) [ 𝑤 / 𝑥 ] 𝜑 ↔ ∀ 𝑦𝐴𝑧𝐵 𝜓 )
37 5 36 bitri ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∀ 𝑦𝐴𝑧𝐵 𝜓 )