Theorem op2nda

Description: Extract the second member of an ordered pair. (See op1sta to extract the first member, op2ndb for an alternate version, and op2nd for the preferred version.) (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Hypotheses	cnvsn.1	$$⊢A\in \mathrm{V}$$
	cnvsn.2	$$⊢B\in \mathrm{V}$$
Assertion	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨A,B⟩\right\}=B$$

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	$$⊢A\in \mathrm{V}$$
2		cnvsn.2	$$⊢B\in \mathrm{V}$$
3	1	rnsnop	$$⊢\mathrm{ran}\left\{⟨A,B⟩\right\}=\left\{B\right\}$$
4	3	unieqi	$$⊢\bigcup \mathrm{ran}\left\{⟨A,B⟩\right\}=\bigcup \left\{B\right\}$$
5	2	unisn	$$⊢\bigcup \left\{B\right\}=B$$
6	4 5	eqtri	$$⊢\bigcup \mathrm{ran}\left\{⟨A,B⟩\right\}=B$$