Metamath Proof Explorer

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 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2nreu.b ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion 2nreu ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝜓 ∧ 𝜒 ) → ¬ ∃! 𝑥 ∈ 𝑋 𝜑 ) )

Proof

Step Hyp Ref Expression
1 2nreu.a ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 2nreu.b ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
3 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝐴 ∈ 𝑋 )
4 simpl2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝐵 ∈ 𝑋 )
5 simprl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜓 )
6 2 sbcieg ⊢ ( 𝐵 ∈ 𝑋 → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ 𝜒 ) )
7 6 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ 𝜒 ) )
8 7 biimprd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) → ( 𝜒 → [ 𝐵 / 𝑥 ] 𝜑 ) )
9 8 adantld ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝜓 ∧ 𝜒 ) → [ 𝐵 / 𝑥 ] 𝜑 ) )
10 9 imp ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → [ 𝐵 / 𝑥 ] 𝜑 )
11 5 10 jca ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) )
12 simpl3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝐴 ≠ 𝐵 )
13 simp1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ∈ 𝑋 )
14 simp2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → 𝐵 ∈ 𝑋 )
15 simp3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) )
16 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ [ 𝐴 / 𝑥 ] 𝑥 ≠ 𝑦 ) )
17 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
18 1 sbcieg ⊢ ( 𝐴 ∈ 𝑋 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
19 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
20 19 sbcgf ⊢ ( 𝐴 ∈ 𝑋 → ( [ 𝐴 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
21 18 20 anbi12d ⊢ ( 𝐴 ∈ 𝑋 → ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
22 17 21 syl5bb ⊢ ( 𝐴 ∈ 𝑋 → ( [ 𝐴 / 𝑥 ] ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
23 sbcne12 ⊢ ( [ 𝐴 / 𝑥 ] 𝑥 ≠ 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑥 ≠ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 )
24 csbvarg ⊢ ( 𝐴 ∈ 𝑋 → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )
25 csbconstg ⊢ ( 𝐴 ∈ 𝑋 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
26 24 25 neeq12d ⊢ ( 𝐴 ∈ 𝑋 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑥 ≠ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ↔ 𝐴 ≠ 𝑦 ) )
27 23 26 syl5bb ⊢ ( 𝐴 ∈ 𝑋 → ( [ 𝐴 / 𝑥 ] 𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦 ) )
28 22 27 anbi12d ⊢ ( 𝐴 ∈ 𝑋 → ( ( [ 𝐴 / 𝑥 ] ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ [ 𝐴 / 𝑥 ] 𝑥 ≠ 𝑦 ) ↔ ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝑦 ) ) )
29 16 28 syl5bb ⊢ ( 𝐴 ∈ 𝑋 → ( [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝑦 ) ) )
30 29 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝑦 ) ) )
31 30 sbcbidv ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ↔ [ 𝐵 / 𝑦 ] ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝑦 ) ) )
32 sbcan ⊢ ( [ 𝐵 / 𝑦 ] ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝑦 ) ↔ ( [ 𝐵 / 𝑦 ] ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ [ 𝐵 / 𝑦 ] 𝐴 ≠ 𝑦 ) )
33 sbcan ⊢ ( [ 𝐵 / 𝑦 ] ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝐵 / 𝑦 ] 𝜓 ∧ [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
34 sbcg ⊢ ( 𝐵 ∈ 𝑋 → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜓 ) )
35 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
36 35 sbcbii ⊢ ( [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 )
37 sbccow ⊢ ( [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜑 )
38 37 a1i ⊢ ( 𝐵 ∈ 𝑋 → ( [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜑 ) )
39 36 38 syl5bb ⊢ ( 𝐵 ∈ 𝑋 → ( [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜑 ) )
40 34 39 anbi12d ⊢ ( 𝐵 ∈ 𝑋 → ( ( [ 𝐵 / 𝑦 ] 𝜓 ∧ [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ) )
41 40 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( ( [ 𝐵 / 𝑦 ] 𝜓 ∧ [ 𝐵 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ) )
42 33 41 syl5bb ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( [ 𝐵 / 𝑦 ] ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ) )
43 sbcne12 ⊢ ( [ 𝐵 / 𝑦 ] 𝐴 ≠ 𝑦 ↔ ⦋ 𝐵 / 𝑦 ⦌ 𝐴 ≠ ⦋ 𝐵 / 𝑦 ⦌ 𝑦 )
44 csbconstg ⊢ ( 𝐵 ∈ 𝑋 → ⦋ 𝐵 / 𝑦 ⦌ 𝐴 = 𝐴 )
45 csbvarg ⊢ ( 𝐵 ∈ 𝑋 → ⦋ 𝐵 / 𝑦 ⦌ 𝑦 = 𝐵 )
46 44 45 neeq12d ⊢ ( 𝐵 ∈ 𝑋 → ( ⦋ 𝐵 / 𝑦 ⦌ 𝐴 ≠ ⦋ 𝐵 / 𝑦 ⦌ 𝑦 ↔ 𝐴 ≠ 𝐵 ) )
47 46 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( ⦋ 𝐵 / 𝑦 ⦌ 𝐴 ≠ ⦋ 𝐵 / 𝑦 ⦌ 𝑦 ↔ 𝐴 ≠ 𝐵 ) )
48 43 47 syl5bb ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( [ 𝐵 / 𝑦 ] 𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐵 ) )
49 42 48 anbi12d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( ( [ 𝐵 / 𝑦 ] ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ [ 𝐵 / 𝑦 ] 𝐴 ≠ 𝑦 ) ↔ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) )
50 32 49 syl5bb ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( [ 𝐵 / 𝑦 ] ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝑦 ) ↔ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) )
51 31 50 bitrd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) )
52 15 51 mpbird ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
53 rspesbca ⊢ ( ( 𝐵 ∈ 𝑋 ∧ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑦 ∈ 𝑋 [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
54 14 52 53 syl2anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑦 ∈ 𝑋 [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
55 sbcrex ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑋 [ 𝐴 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
56 54 55 sylibr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
57 rspesbca ⊢ ( ( 𝐴 ∈ 𝑋 ∧ [ 𝐴 / 𝑥 ] ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
58 13 56 57 syl2anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝜓 ∧ [ 𝐵 / 𝑥 ] 𝜑 ) ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
59 3 4 11 12 58 syl112anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
60 pm4.61 ⊢ ( ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ¬ 𝑥 = 𝑦 ) )
61 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
62 61 bicomi ⊢ ( ¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦 )
63 62 anbi2i ⊢ ( ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
64 60 63 bitri ⊢ ( ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
65 64 2rexbii ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ∧ 𝑥 ≠ 𝑦 ) )
66 59 65 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
67 66 olcd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝜑 ∨ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
68 ianor ⊢ ( ¬ ( ∃ 𝑥 ∈ 𝑋 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( ¬ ∃ 𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
69 rexnal2 ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
70 69 bicomi ⊢ ( ¬ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
71 70 orbi2i ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( ¬ ∃ 𝑥 ∈ 𝑋 𝜑 ∨ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
72 68 71 bitri ⊢ ( ¬ ( ∃ 𝑥 ∈ 𝑋 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ↔ ( ¬ ∃ 𝑥 ∈ 𝑋 𝜑 ∨ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
73 reu2 ⊢ ( ∃! 𝑥 ∈ 𝑋 𝜑 ↔ ( ∃ 𝑥 ∈ 𝑋 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
74 72 73 xchnxbir ⊢ ( ¬ ∃! 𝑥 ∈ 𝑋 𝜑 ↔ ( ¬ ∃ 𝑥 ∈ 𝑋 𝜑 ∨ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
75 67 74 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → ¬ ∃! 𝑥 ∈ 𝑋 𝜑 )
76 75 ex ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝜓 ∧ 𝜒 ) → ¬ ∃! 𝑥 ∈ 𝑋 𝜑 ) )