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

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( B \ { C , D , E } ) <-> ( A e. B /\ -. A e. { C , D , E } ) )
2		eltpg	|- ( A e. B -> ( A e. { C , D , E } <-> ( A = C \/ A = D \/ A = E ) ) )
3	2	notbid	|- ( A e. B -> ( -. A e. { 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 e. B -> ( -. A e. { C , D , E } <-> ( A =/= C /\ A =/= D /\ A =/= E ) ) )
6	5	pm5.32i	|- ( ( A e. B /\ -. A e. { C , D , E } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D /\ A =/= E ) ) )
7	1 6	bitri	|- ( A e. ( B \ { C , D , E } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D /\ A =/= E ) ) )