Theorem sbabel 1189

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 group(s):   w,A   x,w   x,z   y,z

Proof of Theorem sbabel

Step	Hyp	Ref	Expression
1		sbex 998	. . 3 ⊢ ([y / x]∃v(v = {z∣φ} ∧ v ∈ A) ↔ ∃v[y / x](v = {z∣φ} ∧ v ∈ A))
2		sban 889	. . . . 5 ⊢ ([y / x](v = {z∣φ} ∧ v ∈ A) ↔ ([y / x]v = {z∣φ} ∧ [y / x]v ∈ A))
3		ax-17 925	. . . . . . . . . 10 ⊢ (w ∈ v → ∀x w ∈ v)
4		sbabel.1	. . . . . . . . . 10 ⊢ (w ∈ A → ∀x w ∈ A)
5	3, 4	hbel 1172	. . . . . . . . 9 ⊢ (v ∈ A → ∀x v ∈ A)
6	5	sbf 870	. . . . . . . 8 ⊢ ([y / x]v ∈ A ↔ v ∈ A)
7	6	anbi2i 367	. . . . . . 7 ⊢ (([y / x]v = {z∣φ} ∧ [y / x]v ∈ A) ↔ ([y / x]v = {z∣φ} ∧ v ∈ A))
8	7	bicomi 150	. . . . . 6 ⊢ (([y / x]v = {z∣φ} ∧ v ∈ A) ↔ ([y / x]v = {z∣φ} ∧ [y / x]v ∈ A))
9		sbal 997	. . . . . . . . 9 ⊢ ([y / x]∀z(z ∈ v ↔ φ) ↔ ∀z[y / x](z ∈ v ↔ φ))
10		sbbi 890	. . . . . . . . . . 11 ⊢ ([y / x](z ∈ v ↔ φ) ↔ ([y / x]z ∈ v ↔ [y / x]φ))
11		ax-17 925	. . . . . . . . . . . . . 14 ⊢ (z ∈ v → ∀x z ∈ v)
12	11	sbf 870	. . . . . . . . . . . . 13 ⊢ ([y / x]z ∈ v ↔ z ∈ v)
13	12	bibi1i 461	. . . . . . . . . . . 12 ⊢ (([y / x]z ∈ v ↔ [y / x]φ) ↔ (z ∈ v ↔ [y / x]φ))
14	13	bicomi 150	. . . . . . . . . . 11 ⊢ ((z ∈ v ↔ [y / x]φ) ↔ ([y / x]z ∈ v ↔ [y / x]φ))
15	10, 14	bitr4 154	. . . . . . . . . 10 ⊢ ([y / x](z ∈ v ↔ φ) ↔ (z ∈ v ↔ [y / x]φ))
16	15	bial 695	. . . . . . . . 9 ⊢ (∀z[y / x](z ∈ v ↔ φ) ↔ ∀z(z ∈ v ↔ [y / x]φ))
17	9, 16	bitr 151	. . . . . . . 8 ⊢ ([y / x]∀z(z ∈ v ↔ φ) ↔ ∀z(z ∈ v ↔ [y / x]φ))
18		cleqab 1174	. . . . . . . . 9 ⊢ (v = {z∣φ} ↔ ∀z(z ∈ v ↔ φ))
19	18	bisb 855	. . . . . . . 8 ⊢ ([y / x]v = {z∣φ} ↔ [y / x]∀z(z ∈ v ↔ φ))
20		cleqab 1174	. . . . . . . 8 ⊢ (v = {z∣[y / x]φ} ↔ ∀z(z ∈ v ↔ [y / x]φ))
21	17, 19, 20	3bitr4 158	. . . . . . 7 ⊢ ([y / x]v = {z∣φ} ↔ v = {z∣[y / x]φ})
22	21	anbi1i 368	. . . . . 6 ⊢ (([y / x]v = {z∣φ} ∧ v ∈ A) ↔ (v = {z∣[y / x]φ} ∧ v ∈ A))
23	8, 22	bitr3 153	. . . . 5 ⊢ (([y / x]v = {z∣φ} ∧ [y / x]v ∈ A) ↔ (v = {z∣[y / x]φ} ∧ v ∈ A))
24	2, 23	bitr 151	. . . 4 ⊢ ([y / x](v = {z∣φ} ∧ v ∈ A) ↔ (v = {z∣[y / x]φ} ∧ v ∈ A))
25	24	biex 733	. . 3 ⊢ (∃v[y / x](v = {z∣φ} ∧ v ∈ A) ↔ ∃v(v = {z∣[y / x]φ} ∧ v ∈ A))
26	1, 25	bitr 151	. 2 ⊢ ([y / x]∃v(v = {z∣φ} ∧ v ∈ A) ↔ ∃v(v = {z∣[y / x]φ} ∧ v ∈ A))
27		df-clel 1099	. . 3 ⊢ ({z∣φ} ∈ A ↔ ∃v(v = {z∣φ} ∧ v ∈ A))
28	27	bisb 855	. 2 ⊢ ([y / x]{z∣φ} ∈ A ↔ [y / x]∃v(v = {z∣φ} ∧ v ∈ A))
29		df-clel 1099	. 2 ⊢ ({z∣[y / x]φ} ∈ A ↔ ∃v(v = {z∣[y / x]φ} ∧ v ∈ A))
30	26, 28, 29	3bitr4 158	1 ⊢ ([y / x]{z∣φ} ∈ A ↔ {z∣[y / x]φ} ∈ A)

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wel 803  [wsb 852  {cab 1090   = wceq 1091   ∈ wcel 1092

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099

metamath.org