Theorem moim

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 22-Apr-1995)

	Ref	Expression
Assertion	moim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃* 𝑥 𝜓 → ∃* 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		imim1	⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) ) )
2	1	al2imi	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
3	2	eximdv	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑦 ∀ 𝑥 ( 𝜓 → 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
4		dfmo	⊢ ( ∃* 𝑥 𝜓 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜓 → 𝑥 = 𝑦 ) )
5		dfmo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
6	3 4 5	3imtr4g	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃* 𝑥 𝜓 → ∃* 𝑥 𝜑 ) )