Metamath Proof Explorer


Theorem eldiftp

Description: Membership in a set with three elements removed. Similar to eldifsn and eldifpr . (Contributed by David A. Wheeler, 22-Jul-2017)

Ref Expression
Assertion eldiftp A B C D E A B A C A D A E

Proof

Step Hyp Ref Expression
1 eldif A B C D E A B ¬ A C D E
2 eltpg A B A C D E A = C A = D A = E
3 2 notbid A B ¬ A C D E ¬ A = C A = D A = E
4 ne3anior A C A D A E ¬ A = C A = D A = E
5 3 4 bitr4di A B ¬ A C D E A C A D A E
6 5 pm5.32i A B ¬ A C D E A B A C A D A E
7 1 6 bitri A B C D E A B A C A D A E