Metamath Proof Explorer


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