Theorem 2nreu 4402

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 1210	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ∈ 𝑋)
2		simpl2 1211	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐵 ∈ 𝑋)
3		simprl 783	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝜓)
4		2nreu.b	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
5	4	sbcieg 3778	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
6	5	3ad2ant2 1152	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
7	6	biimprd 251	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → (𝜒 → [𝐵 / 𝑥]𝜑))
8	7	adantld 496	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → [𝐵 / 𝑥]𝜑))
9	8	imp 412	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → [𝐵 / 𝑥]𝜑)
10	3, 9	jca 521	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (𝜓 ∧ [𝐵 / 𝑥]𝜑))
11		simpl3 1212	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ≠ 𝐵)
12		simp1 1154	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ 𝑋)
13		simp2 1155	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ 𝑋)
14		simp3 1156	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))
15		sbcan 3788	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦))
16		sbcan 3788	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17		2nreu.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
18	17	sbcieg 3778	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
19		nfs1v 2193	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
20	19	sbcgf 3809	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
21	18, 20	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
22	16, 21	bitrid 286	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23		sbcne12 4373	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ ⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦)
24		csbvarg 4392	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
25		csbconstg 3866	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦)
26	24, 25	neeq12d 3017	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦 ↔ 𝐴 ≠ 𝑦))
27	23, 26	bitrid 286	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦))
28	22, 27	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
29	15, 28	bitrid 286	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
30	29	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
31	30	sbcbidv 3794	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
32		sbcan 3788	. . . . . . . . . . . 12 ⊢ ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦))
33		sbcan 3788	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34		sbcg 3811	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦]𝜓 ↔ 𝜓))
35		sbsbc 3743	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
36	35	sbcbii 3795	. . . . . . . . . . . . . . . . 17 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37		sbccow 3762	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)
38	37	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
39	36, 38	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
40	34, 39	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
41	40	3ad2ant2 1152	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
42	33, 41	bitrid 286	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
43		sbcne12 4373	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ ⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦)
44		csbconstg 3866	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝐴 = 𝐴)
45		csbvarg 4392	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝑦 = 𝐵)
46	44, 45	neeq12d 3017	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
47	46	3ad2ant2 1152	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
48	43, 47	bitrid 286	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐵))
49	42, 48	anbi12d 644	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
50	32, 49	bitrid 286	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
51	31, 50	bitrd 282	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
52	14, 51	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
53		rspesbca 3828	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑋 ∧ [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
54	13, 52, 53	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
55		sbcrex 3822	. . . . . . . 8 ⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
56	54, 55	sylibr 237	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
57		rspesbca 3828	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
58	12, 56, 57	syl2anc 596	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
59	1, 2, 10, 11, 58	syl112anc 1401	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
60		pm4.61 410	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61		df-ne 2957	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
62	61	bicomi 227	. . . . . . . 8 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
63	62	anbi2i 635	. . . . . . 7 ⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
64	60, 63	bitri 278	. . . . . 6 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
65	64	2rexbii 3139	. . . . 5 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
66	59, 65	sylibr 237	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
67	66	olcd 888	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68		ianor 997	. . . . 5 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69		rexnal2 3145	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
70	69	bicomi 227	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
71	70	orbi2i 926	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
72	68, 71	bitri 278	. . . 4 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73		reu2 3683	. . . 4 ⊢ (∃!𝑥 ∈ 𝑋 𝜑 ↔ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
74	72, 73	xchnxbir 336	. . 3 ⊢ (¬ ∃!𝑥 ∈ 𝑋 𝜑 ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
75	67, 74	sylibr 237	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)
76	75	ex 418	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  [wsb 2099   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364  [wsbc 3739  ⦋csb 3847

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-nul 4280

This theorem is used by:  reusq0  15625  addsqn2reu  27761  addsqrexnreu  27762  addsqnreup  27763  addsq2nreurex  27764