Theorem 19.2

Description: Theorem 19.2 of Margaris p. 89. This corresponds to the axiom (D) of modal logic (the other standard formulation being extru ). Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g for a more conventional proof of a more general result, which uses additional axioms. The reverse implication is the defining property of effective nonfreeness (see df-nf ). (Contributed by NM, 2-Aug-2017) Remove dependency on ax-7 . (Revised by Wolf Lammen, 4-Dec-2017)

	Ref	Expression
Assertion	19.2	$$⊢\forall x\phi \to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\phi \to \phi$$
2	1	exgen	$$⊢\exists x\left(\phi \to \phi \right)$$
3	2	19.35i	$$⊢\forall x\phi \to \exists x\phi$$