Metamath Proof Explorer

Theorem oppr

Description: Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023)

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

Step	Hyp	Ref	Expression
1		opthg	\|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
2		preq12	\|- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
3	1 2	biimtrdi	\|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. -> { A , B } = { C , D } ) )

Step

Hyp

Ref

Expression

 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )

 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )

1 2

 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. -> { A , B } = { C , D } ) )