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

Metamath Proof Explorer

Theorem moimi

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006) Remove use of ax-5 . (Revised by Steven Nguyen, 9-May-2023)

		Ref	Expression
	Hypothesis	moimi.1	$⊢ φ \to ψ$
	Assertion	moimi	$⊢ \exists^{} x ψ \to \exists^{} x φ$

Proof

Step	Hyp	Ref	Expression
1		moimi.1	$⊢ φ \to ψ$
2	1	imim1i	$⊢ (ψ \to x = y) \to (φ \to x = y)$
3	2	alimi	$⊢ \forall x (ψ \to x = y) \to \forall x (φ \to x = y)$
4	3	eximi	$⊢ \exists y \forall x (ψ \to x = y) \to \exists y \forall x (φ \to x = y)$
5		df-mo	$⊢ \exists^{*} x ψ \leftrightarrow \exists y \forall x (ψ \to x = y)$
6		df-mo	$⊢ \exists^{*} x φ \leftrightarrow \exists y \forall x (φ \to x = y)$
7	4 5 6	3imtr4i	$⊢ \exists^{} x ψ \to \exists^{} x φ$