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