Theorem bj-nnfext

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

	Ref	Expression
Assertion	bj-nnfext	⊢ ( ∀ 𝑥 Ⅎ' 𝑦 𝜑 → Ⅎ' 𝑦 ∃ 𝑥 𝜑 )

Proof

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