Theorem 2nreu 4393

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 1187	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ∈ 𝑋)
2		simpl2 1188	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐵 ∈ 𝑋)
3		simprl 769	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝜓)
4		2nreu.b	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
5	4	sbcieg 3810	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
6	5	3ad2ant2 1130	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
7	6	biimprd 250	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → (𝜒 → [𝐵 / 𝑥]𝜑))
8	7	adantld 493	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → [𝐵 / 𝑥]𝜑))
9	8	imp 409	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → [𝐵 / 𝑥]𝜑)
10	3, 9	jca 514	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (𝜓 ∧ [𝐵 / 𝑥]𝜑))
11		simpl3 1189	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ≠ 𝐵)
12		simp1 1132	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ 𝑋)
13		simp2 1133	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ 𝑋)
14		simp3 1134	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))
15		sbcan 3821	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦))
16		sbcan 3821	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17		2nreu.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
18	17	sbcieg 3810	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
19		nfs1v 2160	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
20	19	sbcgf 3845	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
21	18, 20	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
22	16, 21	syl5bb 285	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23		sbcne12 4364	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ ⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦)
24		csbvarg 4383	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
25		csbconstg 3902	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦)
26	24, 25	neeq12d 3077	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦 ↔ 𝐴 ≠ 𝑦))
27	23, 26	syl5bb 285	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦))
28	22, 27	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
29	15, 28	syl5bb 285	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
30	29	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
31	30	sbcbidv 3827	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
32		sbcan 3821	. . . . . . . . . . . 12 ⊢ ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦))
33		sbcan 3821	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34		sbcg 3847	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦]𝜓 ↔ 𝜓))
35		sbsbc 3776	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
36	35	sbcbii 3829	. . . . . . . . . . . . . . . . 17 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37		sbccow 3795	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)
38	37	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
39	36, 38	syl5bb 285	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
40	34, 39	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
41	40	3ad2ant2 1130	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
42	33, 41	syl5bb 285	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
43		sbcne12 4364	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ ⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦)
44		csbconstg 3902	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝐴 = 𝐴)
45		csbvarg 4383	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝑦 = 𝐵)
46	44, 45	neeq12d 3077	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
47	46	3ad2ant2 1130	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
48	43, 47	syl5bb 285	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐵))
49	42, 48	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
50	32, 49	syl5bb 285	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
51	31, 50	bitrd 281	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
52	14, 51	mpbird 259	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
53		rspesbca 3864	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑋 ∧ [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
54	13, 52, 53	syl2anc 586	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
55		sbcrex 3858	. . . . . . . 8 ⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
56	54, 55	sylibr 236	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
57		rspesbca 3864	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
58	12, 56, 57	syl2anc 586	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
59	1, 2, 10, 11, 58	syl112anc 1370	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
60		pm4.61 407	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61		df-ne 3017	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
62	61	bicomi 226	. . . . . . . 8 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
63	62	anbi2i 624	. . . . . . 7 ⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
64	60, 63	bitri 277	. . . . . 6 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
65	64	2rexbii 3248	. . . . 5 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
66	59, 65	sylibr 236	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
67	66	olcd 870	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68		ianor 978	. . . . 5 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69		rexnal2 3258	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
70	69	bicomi 226	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
71	70	orbi2i 909	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
72	68, 71	bitri 277	. . . 4 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73		reu2 3716	. . . 4 ⊢ (∃!𝑥 ∈ 𝑋 𝜑 ↔ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
74	72, 73	xchnxbir 335	. . 3 ⊢ (¬ ∃!𝑥 ∈ 𝑋 𝜑 ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
75	67, 74	sylibr 236	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)
76	75	ex 415	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537  [wsb 2069   ∈ wcel 2114   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  [wsbc 3772  ⦋csb 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-nul 4292

This theorem is referenced by:  reusq0  14822  addsqn2reu  26017  addsqrexnreu  26018  addsqnreup  26019  addsq2nreurex  26020