Metamath Proof Explorer

Theorem sbnf2

Description: Two ways of expressing " x is (effectively) not free in ph ". (Contributed by Gérard Lang, 14-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 22-Sep-2018) Avoid ax-13 . (Revised by Wolf Lammen, 30-Jan-2023)

Ref Expression
Assertion sbnf2 ⊢ Ⅎ x φ ↔ ∀ y ∀ z y x φ ↔ z x φ

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ y φ
2 1 sb8ev ⊢ ∃ x φ ↔ ∃ y y x φ
3 nfv ⊢ Ⅎ z φ
4 3 sb8v ⊢ ∀ x φ ↔ ∀ z z x φ
5 2 4 imbi12i ⊢ ∃ x φ → ∀ x φ ↔ ∃ y y x φ → ∀ z z x φ
6 df-nf ⊢ Ⅎ x φ ↔ ∃ x φ → ∀ x φ
7 pm11.53v ⊢ ∀ y ∀ z y x φ → z x φ ↔ ∃ y y x φ → ∀ z z x φ
8 5 6 7 3bitr4i ⊢ Ⅎ x φ ↔ ∀ y ∀ z y x φ → z x φ
9 3 sb8ev ⊢ ∃ x φ ↔ ∃ z z x φ
10 1 sb8v ⊢ ∀ x φ ↔ ∀ y y x φ
11 9 10 imbi12i ⊢ ∃ x φ → ∀ x φ ↔ ∃ z z x φ → ∀ y y x φ
12 pm11.53v ⊢ ∀ z ∀ y z x φ → y x φ ↔ ∃ z z x φ → ∀ y y x φ
13 11 6 12 3bitr4i ⊢ Ⅎ x φ ↔ ∀ z ∀ y z x φ → y x φ
14 alcom ⊢ ∀ z ∀ y z x φ → y x φ ↔ ∀ y ∀ z z x φ → y x φ
15 13 14 bitri ⊢ Ⅎ x φ ↔ ∀ y ∀ z z x φ → y x φ
16 8 15 anbi12i ⊢ Ⅎ x φ ∧ Ⅎ x φ ↔ ∀ y ∀ z y x φ → z x φ ∧ ∀ y ∀ z z x φ → y x φ
17 pm4.24 ⊢ Ⅎ x φ ↔ Ⅎ x φ ∧ Ⅎ x φ
18 2albiim ⊢ ∀ y ∀ z y x φ ↔ z x φ ↔ ∀ y ∀ z y x φ → z x φ ∧ ∀ y ∀ z z x φ → y x φ
19 16 17 18 3bitr4i ⊢ Ⅎ x φ ↔ ∀ y ∀ z y x φ ↔ z x φ