Metamath Proof Explorer


Theorem ax6e2ndeqALT

Description: "At least two sets exist" expressed in the form of dtru is logically equivalent to the same expressed in a form similar to ax6e if dtru is false implies u = v . Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2ndeqALT ¬ x x = y u = v x y x = u y = v

Proof

Step Hyp Ref Expression
1 ax6e2nd ¬ x x = y x y x = u y = v
2 ax6e2eq x x = y u = v x y x = u y = v
3 1 a1d ¬ x x = y u = v x y x = u y = v
4 exmid x x = y ¬ x x = y
5 jao x x = y u = v x y x = u y = v ¬ x x = y u = v x y x = u y = v x x = y ¬ x x = y u = v x y x = u y = v
6 5 3imp x x = y u = v x y x = u y = v ¬ x x = y u = v x y x = u y = v x x = y ¬ x x = y u = v x y x = u y = v
7 2 3 4 6 mp3an u = v x y x = u y = v
8 1 7 jaoi ¬ x x = y u = v x y x = u y = v
9 hbnae ¬ x x = y y ¬ x x = y
10 9 eximi y ¬ x x = y y y ¬ x x = y
11 nfa1 y y ¬ x x = y
12 11 19.9 y y ¬ x x = y y ¬ x x = y
13 10 12 sylib y ¬ x x = y y ¬ x x = y
14 sp y ¬ x x = y ¬ x x = y
15 13 14 syl y ¬ x x = y ¬ x x = y
16 excom x y x = u y = v y x x = u y = v
17 nfa1 x x x = y
18 17 nfn x ¬ x x = y
19 18 19.9 x ¬ x x = y ¬ x x = y
20 id u v u v
21 simpr u v x = u y = v x = u y = v
22 simpl x = u y = v x = u
23 21 22 syl u v x = u y = v x = u
24 pm13.181 x = u u v x v
25 24 ancoms u v x = u x v
26 20 23 25 syl2an2r u v x = u y = v x v
27 simpr x = u y = v y = v
28 21 27 syl u v x = u y = v y = v
29 neeq2 y = v x y x v
30 29 biimparc x v y = v x y
31 26 28 30 syl2anc u v x = u y = v x y
32 df-ne x y ¬ x = y
33 32 bicomi ¬ x = y x y
34 sp x x = y x = y
35 34 con3i ¬ x = y ¬ x x = y
36 33 35 sylbir x y ¬ x x = y
37 31 36 syl u v x = u y = v ¬ x x = y
38 37 ex u v x = u y = v ¬ x x = y
39 38 alrimiv u v x x = u y = v ¬ x x = y
40 exim x x = u y = v ¬ x x = y x x = u y = v x ¬ x x = y
41 39 40 syl u v x x = u y = v x ¬ x x = y
42 imbi2 x ¬ x x = y ¬ x x = y x x = u y = v x ¬ x x = y x x = u y = v ¬ x x = y
43 42 biimpa x ¬ x x = y ¬ x x = y x x = u y = v x ¬ x x = y x x = u y = v ¬ x x = y
44 19 41 43 sylancr u v x x = u y = v ¬ x x = y
45 44 alrimiv u v y x x = u y = v ¬ x x = y
46 exim y x x = u y = v ¬ x x = y y x x = u y = v y ¬ x x = y
47 45 46 syl u v y x x = u y = v y ¬ x x = y
48 imbi1 x y x = u y = v y x x = u y = v x y x = u y = v y ¬ x x = y y x x = u y = v y ¬ x x = y
49 48 biimpar x y x = u y = v y x x = u y = v y x x = u y = v y ¬ x x = y x y x = u y = v y ¬ x x = y
50 16 47 49 sylancr u v x y x = u y = v y ¬ x x = y
51 pm3.34 y ¬ x x = y ¬ x x = y x y x = u y = v y ¬ x x = y x y x = u y = v ¬ x x = y
52 15 50 51 sylancr u v x y x = u y = v ¬ x x = y
53 orc ¬ x x = y ¬ x x = y u = v
54 53 imim2i x y x = u y = v ¬ x x = y x y x = u y = v ¬ x x = y u = v
55 52 54 syl u v x y x = u y = v ¬ x x = y u = v
56 55 idiALT u v x y x = u y = v ¬ x x = y u = v
57 id u = v u = v
58 ax-1 u = v x y x = u y = v u = v
59 57 58 syl u = v x y x = u y = v u = v
60 olc u = v ¬ x x = y u = v
61 60 imim2i x y x = u y = v u = v x y x = u y = v ¬ x x = y u = v
62 59 61 syl u = v x y x = u y = v ¬ x x = y u = v
63 62 idiALT u = v x y x = u y = v ¬ x x = y u = v
64 exmidne u = v u v
65 jao u = v x y x = u y = v ¬ x x = y u = v u v x y x = u y = v ¬ x x = y u = v u = v u v x y x = u y = v ¬ x x = y u = v
66 65 3imp21 u v x y x = u y = v ¬ x x = y u = v u = v x y x = u y = v ¬ x x = y u = v u = v u v x y x = u y = v ¬ x x = y u = v
67 56 63 64 66 mp3an x y x = u y = v ¬ x x = y u = v
68 8 67 impbii ¬ x x = y u = v x y x = u y = v