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