Metamath Proof Explorer

Theorem bj-nnfext

Description: See nfex and bj-nfext . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnfext ⊢ ∀ x Ⅎ' y φ → Ⅎ' y ∃ x φ

Proof

Step Hyp Ref Expression
1 df-bj-nnf ⊢ Ⅎ' y φ ↔ ∃ y φ → φ ∧ φ → ∀ y φ
2 1 albii ⊢ ∀ x Ⅎ' y φ ↔ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ
3 simpl ⊢ ∃ y φ → φ ∧ φ → ∀ y φ → ∃ y φ → φ
4 3 alimi ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∀ x ∃ y φ → φ
5 bj-nnflemee ⊢ ∀ x ∃ y φ → φ → ∃ y ∃ x φ → ∃ x φ
6 4 5 syl ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∃ y ∃ x φ → ∃ x φ
7 2 6 sylbi ⊢ ∀ x Ⅎ' y φ → ∃ y ∃ x φ → ∃ x φ
8 simpr ⊢ ∃ y φ → φ ∧ φ → ∀ y φ → φ → ∀ y φ
9 8 alimi ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∀ x φ → ∀ y φ
10 bj-nnflemae ⊢ ∀ x φ → ∀ y φ → ∃ x φ → ∀ y ∃ x φ
11 9 10 syl ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∃ x φ → ∀ y ∃ x φ
12 2 11 sylbi ⊢ ∀ x Ⅎ' y φ → ∃ x φ → ∀ y ∃ x φ
13 df-bj-nnf ⊢ Ⅎ' y ∃ x φ ↔ ∃ y ∃ x φ → ∃ x φ ∧ ∃ x φ → ∀ y ∃ x φ
14 7 12 13 sylanbrc ⊢ ∀ x Ⅎ' y φ → Ⅎ' y ∃ x φ