Theorem op2nda 6210

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

Hypotheses

Ref	Expression
cnvsn.1	⊢ 𝐴 ∈ V
cnvsn.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
op2nda	⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵

Proof of Theorem op2nda

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  Vcvv 3453  {csn 4579  ⟨cop 4585  ∪ cuni 4862  ran crn 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651  df-dm 5653  df-rn 5654

This theorem is referenced by:  elxp4  7898  elxp5  7899  op2nd  7974  fo2nd  7986  f2ndres  7990  ixpsnf1o  8914  xpassen  9037  xpdom2  9038