Theorem 2nreu 4372

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.)

Hypotheses

Ref	Expression
2nreu.a	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2nreu.b	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
2nreu	⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑋   𝜒,𝑥   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 2nreu

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1189	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ∈ 𝑋)
2		simpl2 1190	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐵 ∈ 𝑋)
3		simprl 767	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝜓)
4		2nreu.b	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
5	4	sbcieg 3751	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
6	5	3ad2ant2 1132	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
7	6	biimprd 247	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → (𝜒 → [𝐵 / 𝑥]𝜑))
8	7	adantld 490	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → [𝐵 / 𝑥]𝜑))
9	8	imp 406	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → [𝐵 / 𝑥]𝜑)
10	3, 9	jca 511	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (𝜓 ∧ [𝐵 / 𝑥]𝜑))
11		simpl3 1191	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ≠ 𝐵)
12		simp1 1134	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ 𝑋)
13		simp2 1135	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ 𝑋)
14		simp3 1136	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))
15		sbcan 3763	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦))
16		sbcan 3763	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17		2nreu.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
18	17	sbcieg 3751	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
19		nfs1v 2155	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
20	19	sbcgf 3789	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
21	18, 20	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
22	16, 21	syl5bb 282	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23		sbcne12 4343	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ ⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦)
24		csbvarg 4362	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
25		csbconstg 3847	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦)
26	24, 25	neeq12d 3004	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦 ↔ 𝐴 ≠ 𝑦))
27	23, 26	syl5bb 282	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦))
28	22, 27	anbi12d 630	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
29	15, 28	syl5bb 282	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
30	29	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
31	30	sbcbidv 3770	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
32		sbcan 3763	. . . . . . . . . . . 12 ⊢ ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦))
33		sbcan 3763	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34		sbcg 3791	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦]𝜓 ↔ 𝜓))
35		sbsbc 3715	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
36	35	sbcbii 3772	. . . . . . . . . . . . . . . . 17 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37		sbccow 3734	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)
38	37	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
39	36, 38	syl5bb 282	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
40	34, 39	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
41	40	3ad2ant2 1132	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
42	33, 41	syl5bb 282	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
43		sbcne12 4343	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ ⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦)
44		csbconstg 3847	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝐴 = 𝐴)
45		csbvarg 4362	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝑦 = 𝐵)
46	44, 45	neeq12d 3004	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
47	46	3ad2ant2 1132	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
48	43, 47	syl5bb 282	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐵))
49	42, 48	anbi12d 630	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
50	32, 49	syl5bb 282	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
51	31, 50	bitrd 278	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
52	14, 51	mpbird 256	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
53		rspesbca 3810	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑋 ∧ [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
54	13, 52, 53	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
55		sbcrex 3804	. . . . . . . 8 ⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
56	54, 55	sylibr 233	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
57		rspesbca 3810	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
58	12, 56, 57	syl2anc 583	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
59	1, 2, 10, 11, 58	syl112anc 1372	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
60		pm4.61 404	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61		df-ne 2943	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
62	61	bicomi 223	. . . . . . . 8 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
63	62	anbi2i 622	. . . . . . 7 ⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
64	60, 63	bitri 274	. . . . . 6 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
65	64	2rexbii 3178	. . . . 5 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
66	59, 65	sylibr 233	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
67	66	olcd 870	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68		ianor 978	. . . . 5 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69		rexnal2 3186	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
70	69	bicomi 223	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
71	70	orbi2i 909	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
72	68, 71	bitri 274	. . . 4 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73		reu2 3655	. . . 4 ⊢ (∃!𝑥 ∈ 𝑋 𝜑 ↔ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
74	72, 73	xchnxbir 332	. . 3 ⊢ (¬ ∃!𝑥 ∈ 𝑋 𝜑 ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
75	67, 74	sylibr 233	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)
76	75	ex 412	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539  [wsb 2068   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  ∃!wreu 3065  [wsbc 3711  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-nul 4254

This theorem is referenced by:  reusq0  15102  addsqn2reu  26494  addsqrexnreu  26495  addsqnreup  26496  addsq2nreurex  26497