Metamath Proof Explorer


Theorem altopth2

Description: Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012)

Ref Expression
Assertion altopth2 B V A B = C D B = D

Proof

Step Hyp Ref Expression
1 altopthsn A B = C D A = C B = D
2 sneqrg B V B = D B = D
3 2 adantld B V A = C B = D B = D
4 1 3 syl5bi B V A B = C D B = D