Metamath Proof Explorer

Theorem bj-sbnf

Description: Move nonfree predicate in and out of substitution; see sbal and sbex . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-sbnf ⊢ z y Ⅎ x φ ↔ Ⅎ x z y φ

Proof

Step Hyp Ref Expression
1 sbim ⊢ z y φ → ∀ x φ ↔ z y φ → z y ∀ x φ
2 sbal ⊢ z y ∀ x φ ↔ ∀ x z y φ
3 2 imbi2i ⊢ z y φ → z y ∀ x φ ↔ z y φ → ∀ x z y φ
4 1 3 bitri ⊢ z y φ → ∀ x φ ↔ z y φ → ∀ x z y φ
5 4 albii ⊢ ∀ x z y φ → ∀ x φ ↔ ∀ x z y φ → ∀ x z y φ
6 nf5 ⊢ Ⅎ x φ ↔ ∀ x φ → ∀ x φ
7 6 sbbii ⊢ z y Ⅎ x φ ↔ z y ∀ x φ → ∀ x φ
8 sbal ⊢ z y ∀ x φ → ∀ x φ ↔ ∀ x z y φ → ∀ x φ
9 7 8 bitri ⊢ z y Ⅎ x φ ↔ ∀ x z y φ → ∀ x φ
10 nf5 ⊢ Ⅎ x z y φ ↔ ∀ x z y φ → ∀ x z y φ
11 5 9 10 3bitr4i ⊢ z y Ⅎ x φ ↔ Ⅎ x z y φ