Theorem 2nreu

Description: If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023)

	Ref	Expression
Hypotheses	2nreu.a	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	2nreu.b	$$⊢x=B\to \left(\phi \leftrightarrow \chi \right)$$
Assertion	2nreu	$$⊢\left(A\in X\wedge B\in X\wedge A\ne B\right)\to \left(\left(\psi \wedge \chi \right)\to \neg \exists !x\in X\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		2nreu.a	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		2nreu.b	$$⊢x=B\to \left(\phi \leftrightarrow \chi \right)$$
3		simpl1	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to A\in X$$
4		simpl2	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to B\in X$$
5		simprl	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \psi$$
6	2	sbcieg	$$⊢B\in X\to \left(\underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \leftrightarrow \chi \right)$$
7	6	3ad2ant2	$$⊢\left(A\in X\wedge B\in X\wedge A\ne B\right)\to \left(\underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \leftrightarrow \chi \right)$$
8	7	biimprd	$$⊢\left(A\in X\wedge B\in X\wedge A\ne B\right)\to \left(\chi \to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$
9	8	adantld	$$⊢\left(A\in X\wedge B\in X\wedge A\ne B\right)\to \left(\left(\psi \wedge \chi \right)\to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$
10	9	imp	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi$$
11	5 10	jca	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$
12		simpl3	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to A\ne B$$
13		simp1	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to A\in X$$
14		simp2	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to B\in X$$
15		simp3	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)$$
16		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \left[y/x\right]\phi \right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\ne y\right)$$
17		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \left[y/x\right]\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[y/x\right]\phi \right)$$
18	1	sbcieg	$$⊢A\in X\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
19		nfs1v	$$⊢Ⅎx\left[y/x\right]\phi$$
20	19	sbcgf	$$⊢A\in X\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[y/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
21	18 20	anbi12d	$$⊢A\in X\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[y/x\right]\phi \right)\leftrightarrow \left(\psi \wedge \left[y/x\right]\phi \right)\right)$$
22	17 21	bitrid	$$⊢A\in X\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \left[y/x\right]\phi \right)\leftrightarrow \left(\psi \wedge \left[y/x\right]\phi \right)\right)$$
23		sbcne12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\ne y\leftrightarrow ⦋A/x⦌x\ne ⦋A/x⦌y$$
24		csbvarg	$$⊢A\in X\to ⦋A/x⦌x=A$$
25		csbconstg	$$⊢A\in X\to ⦋A/x⦌y=y$$
26	24 25	neeq12d	$$⊢A\in X\to \left(⦋A/x⦌x\ne ⦋A/x⦌y\leftrightarrow A\ne y\right)$$
27	23 26	bitrid	$$⊢A\in X\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\ne y\leftrightarrow A\ne y\right)$$
28	22 27	anbi12d	$$⊢A\in X\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \left[y/x\right]\phi \right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\ne y\right)\leftrightarrow \left(\left(\psi \wedge \left[y/x\right]\phi \right)\wedge A\ne y\right)\right)$$
29	16 28	bitrid	$$⊢A\in X\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\leftrightarrow \left(\left(\psi \wedge \left[y/x\right]\phi \right)\wedge A\ne y\right)\right)$$
30	29	3ad2ant1	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\leftrightarrow \left(\left(\psi \wedge \left[y/x\right]\phi \right)\wedge A\ne y\right)\right)$$
31	30	sbcbidv	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(\psi \wedge \left[y/x\right]\phi \right)\wedge A\ne y\right)\right)$$
32		sbcan	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(\psi \wedge \left[y/x\right]\phi \right)\wedge A\ne y\right)\leftrightarrow \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\psi \wedge \left[y/x\right]\phi \right)\wedge \underset{\dot{}}{[}B/y\underset{\dot{}}{]}A\ne y\right)$$
33		sbcan	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\psi \wedge \left[y/x\right]\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \wedge \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left[y/x\right]\phi \right)$$
34		sbcg	$$⊢B\in X\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \psi \right)$$
35		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
36	35	sbcbii	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
37		sbccow	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi$$
38	37	a1i	$$⊢B\in X\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$
39	36 38	bitrid	$$⊢B\in X\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)$$
40	34 39	anbi12d	$$⊢B\in X\to \left(\left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \wedge \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left[y/x\right]\phi \right)\leftrightarrow \left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\right)$$
41	40	3ad2ant2	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \wedge \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left[y/x\right]\phi \right)\leftrightarrow \left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\right)$$
42	33 41	bitrid	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\psi \wedge \left[y/x\right]\phi \right)\leftrightarrow \left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\right)$$
43		sbcne12	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}A\ne y\leftrightarrow ⦋B/y⦌A\ne ⦋B/y⦌y$$
44		csbconstg	$$⊢B\in X\to ⦋B/y⦌A=A$$
45		csbvarg	$$⊢B\in X\to ⦋B/y⦌y=B$$
46	44 45	neeq12d	$$⊢B\in X\to \left(⦋B/y⦌A\ne ⦋B/y⦌y\leftrightarrow A\ne B\right)$$
47	46	3ad2ant2	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(⦋B/y⦌A\ne ⦋B/y⦌y\leftrightarrow A\ne B\right)$$
48	43 47	bitrid	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}A\ne y\leftrightarrow A\ne B\right)$$
49	42 48	anbi12d	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\psi \wedge \left[y/x\right]\phi \right)\wedge \underset{\dot{}}{[}B/y\underset{\dot{}}{]}A\ne y\right)\leftrightarrow \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)$$
50	32 49	bitrid	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(\psi \wedge \left[y/x\right]\phi \right)\wedge A\ne y\right)\leftrightarrow \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)$$
51	31 50	bitrd	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\leftrightarrow \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)$$
52	15 51	mpbird	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
53		rspesbca	$$⊢\left(B\in X\wedge \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\right)\to \exists y\in X\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
54	14 52 53	syl2anc	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \exists y\in X\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
55		sbcrex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\leftrightarrow \exists y\in X\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
56	54 55	sylibr	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
57		rspesbca	$$⊢\left(A\in X\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)\right)\to \exists x\in X\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
58	13 56 57	syl2anc	$$⊢\left(A\in X\wedge B\in X\wedge \left(\left(\psi \wedge \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\phi \right)\wedge A\ne B\right)\right)\to \exists x\in X\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
59	3 4 11 12 58	syl112anc	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \exists x\in X\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
60		pm4.61	$$⊢\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge \neg x=y\right)$$
61		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
62	61	bicomi	$$⊢\neg x=y\leftrightarrow x\ne y$$
63	62	anbi2i	$$⊢\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge \neg x=y\right)\leftrightarrow \left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
64	60 63	bitri	$$⊢\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
65	64	2rexbii	$$⊢\exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \exists x\in X\exists y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\wedge x\ne y\right)$$
66	59 65	sylibr	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
67	66	olcd	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \left(\neg \exists x\in X\phi \vee \exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
68		ianor	$$⊢\neg \left(\exists x\in X\phi \wedge \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)\leftrightarrow \left(\neg \exists x\in X\phi \vee \neg \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
69		rexnal2	$$⊢\exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \neg \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
70	69	bicomi	$$⊢\neg \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
71	70	orbi2i	$$⊢\left(\neg \exists x\in X\phi \vee \neg \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)\leftrightarrow \left(\neg \exists x\in X\phi \vee \exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
72	68 71	bitri	$$⊢\neg \left(\exists x\in X\phi \wedge \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)\leftrightarrow \left(\neg \exists x\in X\phi \vee \exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
73		reu2	$$⊢\exists !x\in X\phi \leftrightarrow \left(\exists x\in X\phi \wedge \forall x\in X\forall y\in X\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
74	72 73	xchnxbir	$$⊢\neg \exists !x\in X\phi \leftrightarrow \left(\neg \exists x\in X\phi \vee \exists x\in X\exists y\in X\neg \left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
75	67 74	sylibr	$$⊢\left(\left(A\in X\wedge B\in X\wedge A\ne B\right)\wedge \left(\psi \wedge \chi \right)\right)\to \neg \exists !x\in X\phi$$
76	75	ex	$$⊢\left(A\in X\wedge B\in X\wedge A\ne B\right)\to \left(\left(\psi \wedge \chi \right)\to \neg \exists !x\in X\phi \right)$$