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	$$⊢x=X\to \left(\psi \leftrightarrow \chi \right)$$
	nrmod.2	$$⊢x=Y\to \left(\psi \leftrightarrow \theta \right)$$
	nrmod.x	$$⊢\phi \to X\in A$$
	nrmod.y	$$⊢\phi \to Y\in A$$
	nrmod.3	$$⊢\phi \to \chi$$
	nrmod.4	$$⊢\phi \to \theta$$
	nrmod.5	$$⊢\phi \to X\ne Y$$
Assertion	nrmod	$$⊢\phi \to \neg {\exists }^{*}x\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		nrmod.1	$$⊢x=X\to \left(\psi \leftrightarrow \chi \right)$$
2		nrmod.2	$$⊢x=Y\to \left(\psi \leftrightarrow \theta \right)$$
3		nrmod.x	$$⊢\phi \to X\in A$$
4		nrmod.y	$$⊢\phi \to Y\in A$$
5		nrmod.3	$$⊢\phi \to \chi$$
6		nrmod.4	$$⊢\phi \to \theta$$
7		nrmod.5	$$⊢\phi \to X\ne Y$$
8	7	neneqd	$$⊢\phi \to \neg X=Y$$
9	4 6	jca	$$⊢\phi \to \left(Y\in A\wedge \theta \right)$$
10	8 9	2thd	$$⊢\phi \to \left(\neg X=Y\leftrightarrow \left(Y\in A\wedge \theta \right)\right)$$
11		nbbn	$$⊢\left(\neg X=Y\leftrightarrow \left(Y\in A\wedge \theta \right)\right)\leftrightarrow \neg \left(X=Y\leftrightarrow \left(Y\in A\wedge \theta \right)\right)$$
12	10 11	sylib	$$⊢\phi \to \neg \left(X=Y\leftrightarrow \left(Y\in A\wedge \theta \right)\right)$$
13	3 5	jca	$$⊢\phi \to \left(X\in A\wedge \chi \right)$$
14	13	biantrud	$$⊢\phi \to \left({\exists }^{*}x\in A\psi \leftrightarrow \left({\exists }^{*}x\in A\psi \wedge \left(X\in A\wedge \chi \right)\right)\right)$$
15	1 2	rmob	$$⊢\left({\exists }^{*}x\in A\psi \wedge \left(X\in A\wedge \chi \right)\right)\to \left(X=Y\leftrightarrow \left(Y\in A\wedge \theta \right)\right)$$
16	14 15	biimtrdi	$$⊢\phi \to \left({\exists }^{*}x\in A\psi \to \left(X=Y\leftrightarrow \left(Y\in A\wedge \theta \right)\right)\right)$$
17	12 16	mtod	$$⊢\phi \to \neg {\exists }^{*}x\in A\psi$$