This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )

Proof

Step Hyp Ref Expression
1 elprg 
 |-  ( A e. B -> ( A e. { C , D } <-> ( A = C \/ A = D ) ) )
2 1 notbid 
 |-  ( A e. B -> ( -. A e. { C , D } <-> -. ( A = C \/ A = D ) ) )
3 neanior 
 |-  ( ( A =/= C /\ A =/= D ) <-> -. ( A = C \/ A = D ) )
4 2 3 bitr4di 
 |-  ( A e. B -> ( -. A e. { C , D } <-> ( A =/= C /\ A =/= D ) ) )
5 4 pm5.32i 
 |-  ( ( A e. B /\ -. A e. { C , D } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D ) ) )
6 eldif 
 |-  ( A e. ( B \ { C , D } ) <-> ( A e. B /\ -. A e. { C , D } ) )
7 3anass 
 |-  ( ( A e. B /\ A =/= C /\ A =/= D ) <-> ( A e. B /\ ( A =/= C /\ A =/= D ) ) )
8 5 6 7 3bitr4i 
 |-  ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )