Metamath Proof Explorer


Theorem nepss

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 ABABAABB

Proof

Step Hyp Ref Expression
1 nne ¬ABAAB=A
2 neeq1 AB=AABBAB
3 2 biimprcd ABAB=AABB
4 1 3 syl5bi AB¬ABAABB
5 4 orrd ABABAABB
6 inss1 ABA
7 6 jctl ABAABAABA
8 inss2 ABB
9 8 jctl ABBABBABB
10 7 9 orim12i ABAABBABAABAABBABB
11 5 10 syl ABABAABAABBABB
12 ineq2 A=BAA=AB
13 inidm AA=A
14 12 13 eqtr3di A=BAB=A
15 14 necon3i ABAAB
16 15 adantl ABAABAAB
17 ineq1 A=BAB=BB
18 inidm BB=B
19 17 18 eqtrdi A=BAB=B
20 19 necon3i ABBAB
21 20 adantl ABBABBAB
22 16 21 jaoi ABAABAABBABBAB
23 11 22 impbii ABABAABAABBABB
24 df-pss ABAABAABA
25 df-pss ABBABBABB
26 24 25 orbi12i ABAABBABAABAABBABB
27 23 26 bitr4i ABABAABB