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

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