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 e. V -> ( << A , B >> = << C , D >> -> B = D ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | altopthsn | |- ( << A , B >> = << C , D >> <-> ( { A } = { C } /\ { B } = { D } ) ) |
|
2 | sneqrg | |- ( B e. V -> ( { B } = { D } -> B = D ) ) |
|
3 | 2 | adantld | |- ( B e. V -> ( ( { A } = { C } /\ { B } = { D } ) -> B = D ) ) |
4 | 1 3 | syl5bi | |- ( B e. V -> ( << A , B >> = << C , D >> -> B = D ) ) |