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 ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 , 𝐷 , 𝐸 } ) ↔ ( 𝐴 ∈ 𝐵 ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 , 𝐷 , 𝐸 } ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ { 𝐶 , 𝐷 , 𝐸 } ) )
2 eltpg ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝐶 , 𝐷 , 𝐸 } ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ∨ 𝐴 = 𝐸 ) ) )
3 2 notbid ⊢ ( 𝐴 ∈ 𝐵 → ( ¬ 𝐴 ∈ { 𝐶 , 𝐷 , 𝐸 } ↔ ¬ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ∨ 𝐴 = 𝐸 ) ) )
4 ne3anior ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸 ) ↔ ¬ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ∨ 𝐴 = 𝐸 ) )
5 3 4 bitr4di ⊢ ( 𝐴 ∈ 𝐵 → ( ¬ 𝐴 ∈ { 𝐶 , 𝐷 , 𝐸 } ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸 ) ) )
6 5 pm5.32i ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ { 𝐶 , 𝐷 , 𝐸 } ) ↔ ( 𝐴 ∈ 𝐵 ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸 ) ) )
7 1 6 bitri ⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 , 𝐷 , 𝐸 } ) ↔ ( 𝐴 ∈ 𝐵 ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸 ) ) )