Theorem nrmod

Description: Deduce the negation of a restricted "at most one" quantifier. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	nrmod.1	⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜒 ) )
	nrmod.2	⊢ ( 𝑥 = 𝑌 → ( 𝜓 ↔ 𝜃 ) )
	nrmod.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	nrmod.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	nrmod.3	⊢ ( 𝜑 → 𝜒 )
	nrmod.4	⊢ ( 𝜑 → 𝜃 )
	nrmod.5	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion	nrmod	⊢ ( 𝜑 → ¬ ∃* 𝑥 ∈ 𝐴 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nrmod.1	⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜒 ) )
2		nrmod.2	⊢ ( 𝑥 = 𝑌 → ( 𝜓 ↔ 𝜃 ) )
3		nrmod.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		nrmod.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
5		nrmod.3	⊢ ( 𝜑 → 𝜒 )
6		nrmod.4	⊢ ( 𝜑 → 𝜃 )
7		nrmod.5	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
8	7	neneqd	⊢ ( 𝜑 → ¬ 𝑋 = 𝑌 )
9	4 6	jca	⊢ ( 𝜑 → ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) )
10	8 9	2thd	⊢ ( 𝜑 → ( ¬ 𝑋 = 𝑌 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) ) )
11		nbbn	⊢ ( ( ¬ 𝑋 = 𝑌 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) ) ↔ ¬ ( 𝑋 = 𝑌 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) ) )
12	10 11	sylib	⊢ ( 𝜑 → ¬ ( 𝑋 = 𝑌 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) ) )
13	3 5	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝜒 ) )
14	13	biantrud	⊢ ( 𝜑 → ( ∃* 𝑥 ∈ 𝐴 𝜓 ↔ ( ∃* 𝑥 ∈ 𝐴 𝜓 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝜒 ) ) ) )
15	1 2	rmob	⊢ ( ( ∃* 𝑥 ∈ 𝐴 𝜓 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝜒 ) ) → ( 𝑋 = 𝑌 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) ) )
16	14 15	biimtrdi	⊢ ( 𝜑 → ( ∃* 𝑥 ∈ 𝐴 𝜓 → ( 𝑋 = 𝑌 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝜃 ) ) ) )
17	12 16	mtod	⊢ ( 𝜑 → ¬ ∃* 𝑥 ∈ 𝐴 𝜓 )