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

Metamath Proof Explorer

Theorem prneprprc

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

Ref Expression
Assertion prneprprc 
|- ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. C e. _V ) -> { A , B } =/= { C , D } )

Proof

Step Hyp Ref Expression
1 prnesn 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } =/= { D } )
2 1 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. C e. _V ) -> { A , B } =/= { D } )
3 prprc1 
 |-  ( -. C e. _V -> { C , D } = { D } )
4 3 neeq2d 
 |-  ( -. C e. _V -> ( { A , B } =/= { C , D } <-> { A , B } =/= { D } ) )
5 4 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. C e. _V ) -> ( { A , B } =/= { C , D } <-> { A , B } =/= { D } ) )
6 2 5 mpbird 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. C e. _V ) -> { A , B } =/= { C , D } )