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 
|- ( ( A e. V /\ B e. 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 e. V /\ B e. W /\ A =/= B ) -> -. ( A = C /\ B = C ) )
4 simp1 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> A e. V )
5 simp2 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> B e. W )
6 4 5 preqsnd 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
7 6 necon3abid 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } =/= { C } <-> -. ( A = C /\ B = C ) ) )
8 3 7 mpbird 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } =/= { C } )