This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝐴 ∈ V
	cnvsn.2	⊢ 𝐵 ∈ V
Assertion	op2nda	⊢ ∪ ran { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	⊢ 𝐴 ∈ V
2		cnvsn.2	⊢ 𝐵 ∈ V
3	1	rnsnop	⊢ ran { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 }
4	3	unieqi	⊢ ∪ ran { ⟨ 𝐴 , 𝐵 ⟩ } = ∪ { 𝐵 }
5	2	unisn	⊢ ∪ { 𝐵 } = 𝐵
6	4 5	eqtri	⊢ ∪ ran { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵