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	syl6bbr	|- ( 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 ) )