Description: Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | nepss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nne | |
|
2 | neeq1 | |
|
3 | 2 | biimprcd | |
4 | 1 3 | syl5bi | |
5 | 4 | orrd | |
6 | inss1 | |
|
7 | 6 | jctl | |
8 | inss2 | |
|
9 | 8 | jctl | |
10 | 7 9 | orim12i | |
11 | 5 10 | syl | |
12 | ineq2 | |
|
13 | inidm | |
|
14 | 12 13 | eqtr3di | |
15 | 14 | necon3i | |
16 | 15 | adantl | |
17 | ineq1 | |
|
18 | inidm | |
|
19 | 17 18 | eqtrdi | |
20 | 19 | necon3i | |
21 | 20 | adantl | |
22 | 16 21 | jaoi | |
23 | 11 22 | impbii | |
24 | df-pss | |
|
25 | df-pss | |
|
26 | 24 25 | orbi12i | |
27 | 23 26 | bitr4i | |