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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≠ { 𝐶 } )