Theorem sbabel 1581

Description: Theorem to move a substitution in and out of a class abstraction.

Hypothesis

Ref	Expression
sbabel.1	⊢ (w ∈ A → ∀x w ∈ A)

Assertion

Ref	Expression
sbabel	⊢ ([y / x]{z∣φ} ∈ A ↔ {z∣[y / x]φ} ∈ A)

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

Proof of Theorem sbabel

Step	Hyp	Ref	Expression
1		sbex 1346	. . 3 ⊢ ([y / x]∃v(v = {z∣φ} ⋀ v ∈ A) ↔ ∃v[y / x](v = {z∣φ} ⋀ v ∈ A))
2		sban 1235	. . . . 5 ⊢ ([y / x](v = {z∣φ} ⋀ v ∈ A) ↔ ([y / x]v = {z∣φ} ⋀ [y / x]v ∈ A))
3		sbal 1345	. . . . . . . 8 ⊢ ([y / x]∀z(z ∈ v ↔ φ) ↔ ∀z[y / x](z ∈ v ↔ φ))
4		ax-17 969	. . . . . . . . . . 11 ⊢ (z ∈ v → ∀x z ∈ v)
5	4	sbf 1184	. . . . . . . . . 10 ⊢ ([y / x]z ∈ v ↔ z ∈ v)
6	5	sbrbis 1239	. . . . . . . . 9 ⊢ ([y / x](z ∈ v ↔ φ) ↔ (z ∈ v ↔ [y / x]φ))
7	6	albii 997	. . . . . . . 8 ⊢ (∀z[y / x](z ∈ v ↔ φ) ↔ ∀z(z ∈ v ↔ [y / x]φ))
8	3, 7	bitr 173	. . . . . . 7 ⊢ ([y / x]∀z(z ∈ v ↔ φ) ↔ ∀z(z ∈ v ↔ [y / x]φ))
9		abeq2 1565	. . . . . . . 8 ⊢ (v = {z∣φ} ↔ ∀z(z ∈ v ↔ φ))
10	9	sbbii 1172	. . . . . . 7 ⊢ ([y / x]v = {z∣φ} ↔ [y / x]∀z(z ∈ v ↔ φ))
11		abeq2 1565	. . . . . . 7 ⊢ (v = {z∣[y / x]φ} ↔ ∀z(z ∈ v ↔ [y / x]φ))
12	8, 10, 11	3bitr4 183	. . . . . 6 ⊢ ([y / x]v = {z∣φ} ↔ v = {z∣[y / x]φ})
13		ax-17 969	. . . . . . . 8 ⊢ (w ∈ v → ∀x w ∈ v)
14		sbabel.1	. . . . . . . 8 ⊢ (w ∈ A → ∀x w ∈ A)
15	13, 14	hbel 1563	. . . . . . 7 ⊢ (v ∈ A → ∀x v ∈ A)
16	15	sbf 1184	. . . . . 6 ⊢ ([y / x]v ∈ A ↔ v ∈ A)
17	12, 16	anbi12i 482	. . . . 5 ⊢ (([y / x]v = {z∣φ} ⋀ [y / x]v ∈ A) ↔ (v = {z∣[y / x]φ} ⋀ v ∈ A))
18	2, 17	bitr 173	. . . 4 ⊢ ([y / x](v = {z∣φ} ⋀ v ∈ A) ↔ (v = {z∣[y / x]φ} ⋀ v ∈ A))
19	18	exbii 1049	. . 3 ⊢ (∃v[y / x](v = {z∣φ} ⋀ v ∈ A) ↔ ∃v(v = {z∣[y / x]φ} ⋀ v ∈ A))
20	1, 19	bitr 173	. 2 ⊢ ([y / x]∃v(v = {z∣φ} ⋀ v ∈ A) ↔ ∃v(v = {z∣[y / x]φ} ⋀ v ∈ A))
21		df-clel 1470	. . 3 ⊢ ({z∣φ} ∈ A ↔ ∃v(v = {z∣φ} ⋀ v ∈ A))
22	21	sbbii 1172	. 2 ⊢ ([y / x]{z∣φ} ∈ A ↔ [y / x]∃v(v = {z∣φ} ⋀ v ∈ A))
23		df-clel 1470	. 2 ⊢ ({z∣[y / x]φ} ∈ A ↔ ∃v(v = {z∣[y / x]φ} ⋀ v ∈ A))
24	20, 22, 23	3bitr4 183	1 ⊢ ([y / x]{z∣φ} ∈ A ↔ {z∣[y / x]φ} ∈ A)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  [wsbc 1168  {cab 1461

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-12 966  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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470

Copyright terms: Public domain