Metamath Proof Explorer


Theorem eldifpr

Description: Membership in a set with two elements removed. Similar to eldifsn and eldiftp . (Contributed by Mario Carneiro, 18-Jul-2017)

Ref Expression
Assertion eldifpr A B C D A B A C A D

Proof

Step Hyp Ref Expression
1 elprg A B A C D A = C A = D
2 1 notbid A B ¬ A C D ¬ A = C A = D
3 neanior A C A D ¬ A = C A = D
4 2 3 bitr4di A B ¬ A C D A C A D
5 4 pm5.32i A B ¬ A C D A B A C A D
6 eldif A B C D A B ¬ A C D
7 3anass A B A C A D A B A C A D
8 5 6 7 3bitr4i A B C D A B A C A D