Metamath Proof Explorer


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 V B W A C = B C A = B

Proof

Step Hyp Ref Expression
1 simpl A V B W A V
2 simpr A V B W B W
3 1 2 preq1b A V B W A C = B C A = B
4 3 biimpd A V B W A C = B C A = B