Theorem ralxpf 3277

Description: Version of ralxp 3275 with bound-variable hypotheses.

Hypotheses

Ref	Expression
ralxpf.1	⊢ (φ → ∀yφ)
ralxpf.2	⊢ (φ → ∀zφ)
ralxpf.3	⊢ (ψ → ∀xψ)
ralxpf.4	⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))

Assertion

Ref	Expression
ralxpf	⊢ (∀x ∈ (A × B)φ ↔ ∀y ∈ A ∀z ∈ B ψ)

Distinct variable groups:   x,y,A   x,z,B,y

Proof of Theorem ralxpf

Step	Hyp	Ref	Expression
1		cbvralsv 2017	. 2 ⊢ (∀x ∈ (A × B)φ ↔ ∀w ∈ (A × B)[w / x]φ)
2		cbvralsv 2017	. . . 4 ⊢ (∀z ∈ B [u / y]ψ ↔ ∀v ∈ B [v / z][u / y]ψ)
3	2	ralbii 1714	. . 3 ⊢ (∀u ∈ A ∀z ∈ B [u / y]ψ ↔ ∀u ∈ A ∀v ∈ B [v / z][u / y]ψ)
4		ax-17 1012	. . . 4 ⊢ (∀z ∈ B ψ → ∀u∀z ∈ B ψ)
5		ax-17 1012	. . . . 5 ⊢ (z ∈ B → ∀y z ∈ B)
6		hbs1 1374	. . . . 5 ⊢ ([u / y]ψ → ∀y[u / y]ψ)
7	5, 6	hbral 1733	. . . 4 ⊢ (∀z ∈ B [u / y]ψ → ∀y∀z ∈ B [u / y]ψ)
8		sbequ12 1223	. . . . 5 ⊢ (y = u → (ψ ↔ [u / y]ψ))
9	8	ralbidv 1710	. . . 4 ⊢ (y = u → (∀z ∈ B ψ ↔ ∀z ∈ B [u / y]ψ))
10	4, 7, 9	cbvral 1845	. . 3 ⊢ (∀y ∈ A ∀z ∈ B ψ ↔ ∀u ∈ A ∀z ∈ B [u / y]ψ)
11		visset 1860	. . . . . 6 ⊢ u ∈ V
12		visset 1860	. . . . . 6 ⊢ v ∈ V
13	11, 12	eqvinop 2847	. . . . 5 ⊢ (w = ⟨u, v⟩ ↔ ∃y∃z(w = ⟨y, z⟩ ⋀ ⟨y, z⟩ = ⟨u, v⟩))
14		visset 1860	. . . . . . . 8 ⊢ w ∈ V
15		ax-17 1012	. . . . . . . . 9 ⊢ (x ∈ w → ∀y x ∈ w)
16		ralxpf.1	. . . . . . . . 9 ⊢ (φ → ∀yφ)
17	15, 16	hbsbcg 1998	. . . . . . . 8 ⊢ (w ∈ V → ([w / x]φ → ∀y[w / x]φ))
18	14, 17	ax-mp 7	. . . . . . 7 ⊢ ([w / x]φ → ∀y[w / x]φ)
19		ax-17 1012	. . . . . . . . 9 ⊢ (x ∈ v → ∀y x ∈ v)
20	19, 6	hbsbcg 1998	. . . . . . . 8 ⊢ (v ∈ V → ([v / z][u / y]ψ → ∀y[v / z][u / y]ψ))
21	12, 20	ax-mp 7	. . . . . . 7 ⊢ ([v / z][u / y]ψ → ∀y[v / z][u / y]ψ)
22	18, 21	hbbi 1051	. . . . . 6 ⊢ (([w / x]φ ↔ [v / z][u / y]ψ) → ∀y([w / x]φ ↔ [v / z][u / y]ψ))
23		ax-17 1012	. . . . . . . . . 10 ⊢ (x ∈ w → ∀z x ∈ w)
24		ralxpf.2	. . . . . . . . . 10 ⊢ (φ → ∀zφ)
25	23, 24	hbsbcg 1998	. . . . . . . . 9 ⊢ (w ∈ V → ([w / x]φ → ∀z[w / x]φ))
26	14, 25	ax-mp 7	. . . . . . . 8 ⊢ ([w / x]φ → ∀z[w / x]φ)
27		hbs1 1374	. . . . . . . 8 ⊢ ([v / z][u / y]ψ → ∀z[v / z][u / y]ψ)
28	26, 27	hbbi 1051	. . . . . . 7 ⊢ (([w / x]φ ↔ [v / z][u / y]ψ) → ∀z([w / x]φ ↔ [v / z][u / y]ψ))
29	14	eqvinc 1930	. . . . . . . . 9 ⊢ (w = ⟨y, z⟩ ↔ ∃x(x = w ⋀ x = ⟨y, z⟩))
30		hbs1 1374	. . . . . . . . . . 11 ⊢ ([w / x]φ → ∀x[w / x]φ)
31		ralxpf.3	. . . . . . . . . . 11 ⊢ (ψ → ∀xψ)
32	30, 31	hbbi 1051	. . . . . . . . . 10 ⊢ (([w / x]φ ↔ ψ) → ∀x([w / x]φ ↔ ψ))
33		sbequ12 1223	. . . . . . . . . . . 12 ⊢ (x = w → (φ ↔ [w / x]φ))
34	33	bicomd 532	. . . . . . . . . . 11 ⊢ (x = w → ([w / x]φ ↔ φ))
35		ralxpf.4	. . . . . . . . . . 11 ⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))
36	34, 35	sylan9bb 551	. . . . . . . . . 10 ⊢ ((x = w ⋀ x = ⟨y, z⟩) → ([w / x]φ ↔ ψ))
37	32, 36	19.23ai 1105	. . . . . . . . 9 ⊢ (∃x(x = w ⋀ x = ⟨y, z⟩) → ([w / x]φ ↔ ψ))
38	29, 37	sylbi 206	. . . . . . . 8 ⊢ (w = ⟨y, z⟩ → ([w / x]φ ↔ ψ))
39		visset 1860	. . . . . . . . . 10 ⊢ y ∈ V
40		visset 1860	. . . . . . . . . 10 ⊢ z ∈ V
41	39, 40, 12	opth 2843	. . . . . . . . 9 ⊢ (⟨y, z⟩ = ⟨u, v⟩ ↔ (y = u ⋀ z = v))
42		sbequ12 1223	. . . . . . . . . 10 ⊢ (z = v → ([u / y]ψ ↔ [v / z][u / y]ψ))
43	8, 42	sylan9bb 551	. . . . . . . . 9 ⊢ ((y = u ⋀ z = v) → (ψ ↔ [v / z][u / y]ψ))
44	41, 43	sylbi 206	. . . . . . . 8 ⊢ (⟨y, z⟩ = ⟨u, v⟩ → (ψ ↔ [v / z][u / y]ψ))
45	38, 44	sylan9bb 551	. . . . . . 7 ⊢ ((w = ⟨y, z⟩ ⋀ ⟨y, z⟩ = ⟨u, v⟩) → ([w / x]φ ↔ [v / z][u / y]ψ))
46	28, 45	19.23ai 1105	. . . . . 6 ⊢ (∃z(w = ⟨y, z⟩ ⋀ ⟨y, z⟩ = ⟨u, v⟩) → ([w / x]φ ↔ [v / z][u / y]ψ))
47	22, 46	19.23ai 1105	. . . . 5 ⊢ (∃y∃z(w = ⟨y, z⟩ ⋀ ⟨y, z⟩ = ⟨u, v⟩) → ([w / x]φ ↔ [v / z][u / y]ψ))
48	13, 47	sylbi 206	. . . 4 ⊢ (w = ⟨u, v⟩ → ([w / x]φ ↔ [v / z][u / y]ψ))
49	48	ralxp 3275	. . 3 ⊢ (∀w ∈ (A × B)[w / x]φ ↔ ∀u ∈ A ∀v ∈ B [v / z][u / y]ψ)
50	3, 10, 49	3bitr4ri 191	. 2 ⊢ (∀w ∈ (A × B)[w / x]φ ↔ ∀y ∈ A ∀z ∈ B ψ)
51	1, 50	bitri 180	1 ⊢ (∀x ∈ (A × B)φ ↔ ∀y ∈ A ∀z ∈ B ψ)

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230  ∀wal 995   = wceq 997   ∈ wcel 999  ∃wex 1021  [wsbc 1212  ∀wral 1692  Vcvv 1858  ⟨cop 2463   × cxp 3225

This theorem is referenced by:  foprab2 4177

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-v 1859  df-sbc 1989  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-opab 2722  df-xp 3241

Copyright terms: Public domain