Theorem op2ndb

Description: Extract the second member of an ordered pair. Theorem 5.12(ii) of Monk1 p. 52. (See op1stb to extract the first member, op2nda for an alternate version, and op2nd for the preferred version.) (Contributed by NM, 25-Nov-2003)

	Ref	Expression
Hypotheses	cnvsn.1	|- A e. _V
	cnvsn.2	|- B e. _V
Assertion	op2ndb	|- |^| |^| |^| `' { <. A , B >. } = B

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	|- A e. _V
2		cnvsn.2	|- B e. _V
3	1 2	cnvsn	|- `' { <. A , B >. } = { <. B , A >. }
4	3	inteqi	|- |^| `' { <. A , B >. } = |^| { <. B , A >. }
5		opex	|- <. B , A >. e. _V
6	5	intsn	|- |^| { <. B , A >. } = <. B , A >.
7	4 6	eqtri	|- |^| `' { <. A , B >. } = <. B , A >.
8	7	inteqi	|- |^| |^| `' { <. A , B >. } = |^| <. B , A >.
9	8	inteqi	|- |^| |^| |^| `' { <. A , B >. } = |^| |^| <. B , A >.
10	2 1	op1stb	|- |^| |^| <. B , A >. = B
11	9 10	eqtri	|- |^| |^| |^| `' { <. A , B >. } = B