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 -> ( ps <-> ch ) )
	nrmod.2	|- ( x = Y -> ( ps <-> th ) )
	nrmod.x	|- ( ph -> X e. A )
	nrmod.y	|- ( ph -> Y e. A )
	nrmod.3	|- ( ph -> ch )
	nrmod.4	|- ( ph -> th )
	nrmod.5	|- ( ph -> X =/= Y )
Assertion	nrmod	|- ( ph -> -. E* x e. A ps )

Proof

Step	Hyp	Ref	Expression
1		nrmod.1	|- ( x = X -> ( ps <-> ch ) )
2		nrmod.2	|- ( x = Y -> ( ps <-> th ) )
3		nrmod.x	|- ( ph -> X e. A )
4		nrmod.y	|- ( ph -> Y e. A )
5		nrmod.3	|- ( ph -> ch )
6		nrmod.4	|- ( ph -> th )
7		nrmod.5	|- ( ph -> X =/= Y )
8	7	neneqd	|- ( ph -> -. X = Y )
9	4 6	jca	|- ( ph -> ( Y e. A /\ th ) )
10	8 9	2thd	|- ( ph -> ( -. X = Y <-> ( Y e. A /\ th ) ) )
11		nbbn	|- ( ( -. X = Y <-> ( Y e. A /\ th ) ) <-> -. ( X = Y <-> ( Y e. A /\ th ) ) )
12	10 11	sylib	|- ( ph -> -. ( X = Y <-> ( Y e. A /\ th ) ) )
13	3 5	jca	|- ( ph -> ( X e. A /\ ch ) )
14	13	biantrud	|- ( ph -> ( E* x e. A ps <-> ( E* x e. A ps /\ ( X e. A /\ ch ) ) ) )
15	1 2	rmob	|- ( ( E* x e. A ps /\ ( X e. A /\ ch ) ) -> ( X = Y <-> ( Y e. A /\ th ) ) )
16	14 15	biimtrdi	|- ( ph -> ( E* x e. A ps -> ( X = Y <-> ( Y e. A /\ th ) ) ) )
17	12 16	mtod	|- ( ph -> -. E* x e. A ps )