Theorem sbnf2 2108

Description: Two ways of expressing "x is (effectively) not free in φ." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.)

Assertion

Ref	Expression
sbnf2	⊢ (Ⅎxφ ↔ ∀y∀z([y / x]φ ↔ [z / x]φ))

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

Allowed substitution hint:   φ(x)

Proof of Theorem sbnf2

Step	Hyp	Ref	Expression
1		2albiim 1612	. 2 ⊢ (∀y∀z([y / x]φ ↔ [z / x]φ) ↔ (∀y∀z([y / x]φ → [z / x]φ) ∧ ∀y∀z([z / x]φ → [y / x]φ)))
2		df-nf 1545	. . . . 5 ⊢ (Ⅎxφ ↔ ∀x(φ → ∀xφ))
3		sbhb 2107	. . . . . 6 ⊢ ((φ → ∀xφ) ↔ ∀z(φ → [z / x]φ))
4	3	albii 1566	. . . . 5 ⊢ (∀x(φ → ∀xφ) ↔ ∀x∀z(φ → [z / x]φ))
5		alcom 1737	. . . . 5 ⊢ (∀x∀z(φ → [z / x]φ) ↔ ∀z∀x(φ → [z / x]φ))
6	2, 4, 5	3bitri 262	. . . 4 ⊢ (Ⅎxφ ↔ ∀z∀x(φ → [z / x]φ))
7		nfv 1619	. . . . . . 7 ⊢ Ⅎy(φ → [z / x]φ)
8	7	sb8 2092	. . . . . 6 ⊢ (∀x(φ → [z / x]φ) ↔ ∀y[y / x](φ → [z / x]φ))
9		nfs1v 2106	. . . . . . . 8 ⊢ Ⅎx[z / x]φ
10	9	sblim 2068	. . . . . . 7 ⊢ ([y / x](φ → [z / x]φ) ↔ ([y / x]φ → [z / x]φ))
11	10	albii 1566	. . . . . 6 ⊢ (∀y[y / x](φ → [z / x]φ) ↔ ∀y([y / x]φ → [z / x]φ))
12	8, 11	bitri 240	. . . . 5 ⊢ (∀x(φ → [z / x]φ) ↔ ∀y([y / x]φ → [z / x]φ))
13	12	albii 1566	. . . 4 ⊢ (∀z∀x(φ → [z / x]φ) ↔ ∀z∀y([y / x]φ → [z / x]φ))
14		alcom 1737	. . . 4 ⊢ (∀z∀y([y / x]φ → [z / x]φ) ↔ ∀y∀z([y / x]φ → [z / x]φ))
15	6, 13, 14	3bitri 262	. . 3 ⊢ (Ⅎxφ ↔ ∀y∀z([y / x]φ → [z / x]φ))
16		sbhb 2107	. . . . . 6 ⊢ ((φ → ∀xφ) ↔ ∀y(φ → [y / x]φ))
17	16	albii 1566	. . . . 5 ⊢ (∀x(φ → ∀xφ) ↔ ∀x∀y(φ → [y / x]φ))
18		alcom 1737	. . . . 5 ⊢ (∀x∀y(φ → [y / x]φ) ↔ ∀y∀x(φ → [y / x]φ))
19	2, 17, 18	3bitri 262	. . . 4 ⊢ (Ⅎxφ ↔ ∀y∀x(φ → [y / x]φ))
20		nfv 1619	. . . . . . 7 ⊢ Ⅎz(φ → [y / x]φ)
21	20	sb8 2092	. . . . . 6 ⊢ (∀x(φ → [y / x]φ) ↔ ∀z[z / x](φ → [y / x]φ))
22		nfs1v 2106	. . . . . . . 8 ⊢ Ⅎx[y / x]φ
23	22	sblim 2068	. . . . . . 7 ⊢ ([z / x](φ → [y / x]φ) ↔ ([z / x]φ → [y / x]φ))
24	23	albii 1566	. . . . . 6 ⊢ (∀z[z / x](φ → [y / x]φ) ↔ ∀z([z / x]φ → [y / x]φ))
25	21, 24	bitri 240	. . . . 5 ⊢ (∀x(φ → [y / x]φ) ↔ ∀z([z / x]φ → [y / x]φ))
26	25	albii 1566	. . . 4 ⊢ (∀y∀x(φ → [y / x]φ) ↔ ∀y∀z([z / x]φ → [y / x]φ))
27	19, 26	bitri 240	. . 3 ⊢ (Ⅎxφ ↔ ∀y∀z([z / x]φ → [y / x]φ))
28	15, 27	anbi12i 678	. 2 ⊢ ((Ⅎxφ ∧ Ⅎxφ) ↔ (∀y∀z([y / x]φ → [z / x]φ) ∧ ∀y∀z([z / x]φ → [y / x]φ)))
29		anidm 625	. 2 ⊢ ((Ⅎxφ ∧ Ⅎxφ) ↔ Ⅎxφ)
30	1, 28, 29	3bitr2ri 265	1 ⊢ (Ⅎxφ ↔ ∀y∀z([y / x]φ ↔ [z / x]φ))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  Ⅎwnf 1544  [wsb 1648

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

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  sbnfc2  3197