This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜓 )