Theorem nrmo

Description: "At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Hypothesis	nrmo.1	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜑 )
Assertion	nrmo	⊢ ∃* 𝑥 ∈ 𝐴 𝜑

Proof

Step	Hyp	Ref	Expression
1		nrmo.1	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜑 )
2		mofal	⊢ ∃* 𝑥 ⊥
3	1	imori	⊢ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝜑 )
4		ianor	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝜑 ) )
5	3 4	mpbir	⊢ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
6	5	bifal	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ⊥ )
7	6	mobii	⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃* 𝑥 ⊥ )
8	2 7	mpbir	⊢ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
9		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
10	8 9	mpbir	⊢ ∃* 𝑥 ∈ 𝐴 𝜑