Metamath Proof Explorer

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	⊢ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝜑 → 𝜑 )
2	1	exgen	⊢ ∃ 𝑥 ( 𝜑 → 𝜑 )
3	2	19.35i	⊢ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜑 )