This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prnesn

Description: A proper unordered pair is not a (proper or improper) singleton. (Contributed by AV, 13-Jun-2022)

Ref Expression
Assertion prnesn ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≠ { 𝐶 } )

Proof

Step Hyp Ref Expression
1 eqtr3 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )
2 1 necon3ai ⊢ ( 𝐴 ≠ 𝐵 → ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) )
3 2 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) )
4 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑉 )
5 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑊 )
6 4 5 preqsnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
7 6 necon3abid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ≠ { 𝐶 } ↔ ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
8 3 7 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≠ { 𝐶 } )