Theorem bj-dfnnf2

Description: Alternate definition of df-bj-nnf using only primitive symbols ( -> , -. , A. ) in each conjunct. (Contributed by BJ, 20-Aug-2023)

	Ref	Expression
Assertion	bj-dfnnf2	$$⊢Ⅎ\text{'}x\phi \leftrightarrow \left(\left(\phi \to \forall x\phi \right)\wedge \left(\neg \phi \to \forall x\neg \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-nnf	$$⊢Ⅎ\text{'}x\phi \leftrightarrow \left(\left(\exists x\phi \to \phi \right)\wedge \left(\phi \to \forall x\phi \right)\right)$$
2		eximal	$$⊢\left(\exists x\phi \to \phi \right)\leftrightarrow \left(\neg \phi \to \forall x\neg \phi \right)$$
3	2	anbi2ci	$$⊢\left(\left(\exists x\phi \to \phi \right)\wedge \left(\phi \to \forall x\phi \right)\right)\leftrightarrow \left(\left(\phi \to \forall x\phi \right)\wedge \left(\neg \phi \to \forall x\neg \phi \right)\right)$$
4	1 3	bitri	$$⊢Ⅎ\text{'}x\phi \leftrightarrow \left(\left(\phi \to \forall x\phi \right)\wedge \left(\neg \phi \to \forall x\neg \phi \right)\right)$$