This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.23

Description: Theorem 19.23 of Margaris p. 90. See 19.23v for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016)

		Ref	Expression
	Hypothesis	19.23.1	⊢ Ⅎ 𝑥 𝜓
	Assertion	19.23	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.23.1	⊢ Ⅎ 𝑥 𝜓
2		19.23t	⊢ ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) ) )
3	1 2	ax-mp	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) )