Description: A set A not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | nelpr | ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) ) | |
2 | 1 | notbid | ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) ) |
3 | neanior | ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) | |
4 | 2 3 | bitr4di | ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) ) |