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 } )