Theorem opabsb 2810

Description: The law of concretion in terms of substitutions.

Assertion

Ref	Expression
opabsb	⊢ (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)

Distinct variable groups:   x,y,z   x,w,y

Proof of Theorem opabsb

Step	Hyp	Ref	Expression
1		a9e 1123	. 2 ⊢ ∃y y = w
2		ax-17 969	. . . . 5 ⊢ (v ∈ ⟨z, w⟩ → ∀y v ∈ ⟨z, w⟩)
3		hbopab2 2809	. . . . 5 ⊢ (v ∈ {⟨x, y⟩∣φ} → ∀y v ∈ {⟨x, y⟩∣φ})
4	2, 3	hbel 1563	. . . 4 ⊢ (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} → ∀y⟨z, w⟩ ∈ {⟨x, y⟩∣φ})
5		hbs1 1330	. . . 4 ⊢ ([w / y][z / x]φ → ∀y[w / y][z / x]φ)
6	4, 5	hbbi 1008	. . 3 ⊢ ((⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ) → ∀y(⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ))
7		a9e 1123	. . . 4 ⊢ ∃x x = z
8		ax-17 969	. . . . . 6 ⊢ (y = w → ∀x y = w)
9		ax-17 969	. . . . . . . 8 ⊢ (v ∈ ⟨z, w⟩ → ∀x v ∈ ⟨z, w⟩)
10		hbopab1 2808	. . . . . . . 8 ⊢ (v ∈ {⟨x, y⟩∣φ} → ∀x v ∈ {⟨x, y⟩∣φ})
11	9, 10	hbel 1563	. . . . . . 7 ⊢ (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} → ∀x⟨z, w⟩ ∈ {⟨x, y⟩∣φ})
12		hbs1 1330	. . . . . . . 8 ⊢ ([z / x]φ → ∀x[z / x]φ)
13	12	hbsb 1331	. . . . . . 7 ⊢ ([w / y][z / x]φ → ∀x[w / y][z / x]φ)
14	11, 13	hbbi 1008	. . . . . 6 ⊢ ((⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ) → ∀x(⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ))
15	8, 14	hbim 1005	. . . . 5 ⊢ ((y = w → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)) → ∀x(y = w → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)))
16		opeq12 2485	. . . . . . . . 9 ⊢ ((x = z ⋀ y = w) → ⟨x, y⟩ = ⟨z, w⟩)
17	16	eleq1d 1537	. . . . . . . 8 ⊢ ((x = z ⋀ y = w) → (⟨x, y⟩ ∈ {⟨x, y⟩∣φ} ↔ ⟨z, w⟩ ∈ {⟨x, y⟩∣φ}))
18		opabid 2805	. . . . . . . 8 ⊢ (⟨x, y⟩ ∈ {⟨x, y⟩∣φ} ↔ φ)
19	17, 18	syl5bbr 533	. . . . . . 7 ⊢ ((x = z ⋀ y = w) → (φ ↔ ⟨z, w⟩ ∈ {⟨x, y⟩∣φ}))
20		sbequ12 1179	. . . . . . . 8 ⊢ (x = z → (φ ↔ [z / x]φ))
21		sbequ12 1179	. . . . . . . 8 ⊢ (y = w → ([z / x]φ ↔ [w / y][z / x]φ))
22	20, 21	sylan9bb 539	. . . . . . 7 ⊢ ((x = z ⋀ y = w) → (φ ↔ [w / y][z / x]φ))
23	19, 22	bitr3d 529	. . . . . 6 ⊢ ((x = z ⋀ y = w) → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ))
24	23	ex 373	. . . . 5 ⊢ (x = z → (y = w → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)))
25	15, 24	19.23ai 1062	. . . 4 ⊢ (∃x x = z → (y = w → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)))
26	7, 25	ax-mp 7	. . 3 ⊢ (y = w → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ))
27	6, 26	19.23ai 1062	. 2 ⊢ (∃y y = w → (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ))
28	1, 27	ax-mp 7	1 ⊢ (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 954   ∈ wcel 956  ∃wex 978  [wsbc 1168  ⟨cop 2407  {copab 2661

This theorem is referenced by:  brabsb 2811  inopab 3263  isarep1 3569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-opab 2662

Copyright terms: Public domain