Theorem sbabel 2516

Description: Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.)

Hypothesis

Ref	Expression
sbabel.1	⊢ ℲxA

Assertion

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

Distinct variable groups:   x,z   y,z

Allowed substitution hints:   φ(x,y,z)   A(x,y,z)

Proof of Theorem sbabel

Dummy variable v is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbex 2128	. . 3 ⊢ ([y / x]∃v(v = {z ∣ φ} ∧ v ∈ A) ↔ ∃v[y / x](v = {z ∣ φ} ∧ v ∈ A))
2		sban 2069	. . . . 5 ⊢ ([y / x](v = {z ∣ φ} ∧ v ∈ A) ↔ ([y / x]v = {z ∣ φ} ∧ [y / x]v ∈ A))
3		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎx z ∈ v
4	3	sbf 2026	. . . . . . . . 9 ⊢ ([y / x]z ∈ v ↔ z ∈ v)
5	4	sbrbis 2073	. . . . . . . 8 ⊢ ([y / x](z ∈ v ↔ φ) ↔ (z ∈ v ↔ [y / x]φ))
6	5	sbalv 2129	. . . . . . 7 ⊢ ([y / x]∀z(z ∈ v ↔ φ) ↔ ∀z(z ∈ v ↔ [y / x]φ))
7		abeq2 2459	. . . . . . . 8 ⊢ (v = {z ∣ φ} ↔ ∀z(z ∈ v ↔ φ))
8	7	sbbii 1653	. . . . . . 7 ⊢ ([y / x]v = {z ∣ φ} ↔ [y / x]∀z(z ∈ v ↔ φ))
9		abeq2 2459	. . . . . . 7 ⊢ (v = {z ∣ [y / x]φ} ↔ ∀z(z ∈ v ↔ [y / x]φ))
10	6, 8, 9	3bitr4i 268	. . . . . 6 ⊢ ([y / x]v = {z ∣ φ} ↔ v = {z ∣ [y / x]φ})
11		sbabel.1	. . . . . . . 8 ⊢ ℲxA
12	11	nfcri 2484	. . . . . . 7 ⊢ Ⅎx v ∈ A
13	12	sbf 2026	. . . . . 6 ⊢ ([y / x]v ∈ A ↔ v ∈ A)
14	10, 13	anbi12i 678	. . . . 5 ⊢ (([y / x]v = {z ∣ φ} ∧ [y / x]v ∈ A) ↔ (v = {z ∣ [y / x]φ} ∧ v ∈ A))
15	2, 14	bitri 240	. . . 4 ⊢ ([y / x](v = {z ∣ φ} ∧ v ∈ A) ↔ (v = {z ∣ [y / x]φ} ∧ v ∈ A))
16	15	exbii 1582	. . 3 ⊢ (∃v[y / x](v = {z ∣ φ} ∧ v ∈ A) ↔ ∃v(v = {z ∣ [y / x]φ} ∧ v ∈ A))
17	1, 16	bitri 240	. 2 ⊢ ([y / x]∃v(v = {z ∣ φ} ∧ v ∈ A) ↔ ∃v(v = {z ∣ [y / x]φ} ∧ v ∈ A))
18		df-clel 2349	. . 3 ⊢ ({z ∣ φ} ∈ A ↔ ∃v(v = {z ∣ φ} ∧ v ∈ A))
19	18	sbbii 1653	. 2 ⊢ ([y / x]{z ∣ φ} ∈ A ↔ [y / x]∃v(v = {z ∣ φ} ∧ v ∈ A))
20		df-clel 2349	. 2 ⊢ ({z ∣ [y / x]φ} ∈ A ↔ ∃v(v = {z ∣ [y / x]φ} ∧ v ∈ A))
21	17, 19, 20	3bitr4i 268	1 ⊢ ([y / x]{z ∣ φ} ∈ A ↔ {z ∣ [y / x]φ} ∈ A)

Syntax hints:   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  [wsb 1648   ∈ wcel 1710  {cab 2339  Ⅎwnfc 2477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479

This theorem is referenced by: (None)