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 A V B W A B A B C

Proof

Step Hyp Ref Expression
1 eqtr3 A = C B = C A = B
2 1 necon3ai A B ¬ A = C B = C
3 2 3ad2ant3 A V B W A B ¬ A = C B = C
4 simp1 A V B W A B A V
5 simp2 A V B W A B B W
6 4 5 preqsnd A V B W A B A B = C A = C B = C
7 6 necon3abid A V B W A B A B C ¬ A = C B = C
8 3 7 mpbird A V B W A B A B C