Theorem op2nda 6179

Description: Extract the second member of an ordered pair. (See op1sta 6176 to extract the first member, op2ndb 6178 for an alternate version, and op2nd 7940 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 6175	. . 3 ⊢ ran {⟨𝐴, 𝐵⟩} = {𝐵}
3	2	unieqi 4850	. 2 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = ∪ {𝐵}
4		cnvsn.2	. . 3 ⊢ 𝐵 ∈ V
5	4	unisn 4857	. 2 ⊢ ∪ {𝐵} = 𝐵
6	3, 5	eqtri 2762	1 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3431  {csn 4555  ⟨cop 4561  ∪ cuni 4838  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  elxp4  7862  elxp5  7863  op2nd  7940  fo2nd  7952  f2ndres  7956  ixpsnf1o  8876  xpassen  8999  xpdom2  9000