Theorem 2nreu 4443

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 1191	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ∈ 𝑋)
2		simpl2 1192	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐵 ∈ 𝑋)
3		simprl 770	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝜓)
4		2nreu.b	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
5	4	sbcieg 3827	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
6	5	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ([𝐵 / 𝑥]𝜑 ↔ 𝜒))
7	6	biimprd 248	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → (𝜒 → [𝐵 / 𝑥]𝜑))
8	7	adantld 490	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → [𝐵 / 𝑥]𝜑))
9	8	imp 406	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → [𝐵 / 𝑥]𝜑)
10	3, 9	jca 511	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (𝜓 ∧ [𝐵 / 𝑥]𝜑))
11		simpl3 1193	. . . . . 6 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ≠ 𝐵)
12		simp1 1136	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ 𝑋)
13		simp2 1137	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ 𝑋)
14		simp3 1138	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))
15		sbcan 3837	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦))
16		sbcan 3837	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑))
17		2nreu.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
18	17	sbcieg 3827	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
19		nfs1v 2155	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
20	19	sbcgf 3860	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
21	18, 20	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
22	16, 21	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑)))
23		sbcne12 4414	. . . . . . . . . . . . . . . 16 ⊢ ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ ⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦)
24		csbvarg 4433	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
25		csbconstg 3917	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦)
26	24, 25	neeq12d 3001	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑋 → (⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦 ↔ 𝐴 ≠ 𝑦))
27	23, 26	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦))
28	22, 27	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
29	15, 28	bitrid 283	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
30	29	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
31	30	sbcbidv 3844	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦)))
32		sbcan 3837	. . . . . . . . . . . 12 ⊢ ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦))
33		sbcan 3837	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑))
34		sbcg 3862	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦]𝜓 ↔ 𝜓))
35		sbsbc 3791	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
36	35	sbcbii 3845	. . . . . . . . . . . . . . . . 17 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑)
37		sbccow 3810	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)
38	37	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
39	36, 38	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))
40	34, 39	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
41	40	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
42	33, 41	bitrid 283	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑)))
43		sbcne12 4414	. . . . . . . . . . . . . 14 ⊢ ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ ⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦)
44		csbconstg 3917	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝐴 = 𝐴)
45		csbvarg 4433	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝑦 = 𝐵)
46	44, 45	neeq12d 3001	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ 𝑋 → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
47	46	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵))
48	43, 47	bitrid 283	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐵))
49	42, 48	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
50	32, 49	bitrid 283	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
51	31, 50	bitrd 279	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)))
52	14, 51	mpbird 257	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
53		rspesbca 3880	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑋 ∧ [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
54	13, 52, 53	syl2anc 584	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
55		sbcrex 3874	. . . . . . . 8 ⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
56	54, 55	sylibr 234	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
57		rspesbca 3880	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
58	12, 56, 57	syl2anc 584	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
59	1, 2, 10, 11, 58	syl112anc 1375	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
60		pm4.61 404	. . . . . . 7 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦))
61		df-ne 2940	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
62	61	bicomi 224	. . . . . . . 8 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
63	62	anbi2i 623	. . . . . . 7 ⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
64	60, 63	bitri 275	. . . . . 6 ⊢ (¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
65	64	2rexbii 3128	. . . . 5 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦))
66	59, 65	sylibr 234	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
67	66	olcd 874	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
68		ianor 983	. . . . 5 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
69		rexnal2 3134	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
70	69	bicomi 224	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
71	70	orbi2i 912	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
72	68, 71	bitri 275	. . . 4 ⊢ (¬ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
73		reu2 3730	. . . 4 ⊢ (∃!𝑥 ∈ 𝑋 𝜑 ↔ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
74	72, 73	xchnxbir 333	. . 3 ⊢ (¬ ∃!𝑥 ∈ 𝑋 𝜑 ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
75	67, 74	sylibr 234	. 2 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)
76	75	ex 412	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1539  [wsb 2063   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  ∃!wreu 3377  [wsbc 3787  ⦋csb 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-nul 4333

This theorem is referenced by:  reusq0  15502  addsqn2reu  27486  addsqrexnreu  27487  addsqnreup  27488  addsq2nreurex  27489