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

Proof

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