Theorem preqr1g

Description: Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 . (Contributed by AV, 29-Jan-2021) (Revised by AV, 18-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. V /\ B e. W ) -> A e. V )
2		simpr	|- ( ( A e. V /\ B e. W ) -> B e. W )
3	1 2	preq1b	|- ( ( A e. V /\ B e. W ) -> ( { A , C } = { B , C } <-> A = B ) )
4	3	biimpd	|- ( ( A e. V /\ B e. W ) -> ( { A , C } = { B , C } -> A = B ) )