Theorem op2nda 6225

Description: Extract the second member of an ordered pair. (See op1sta 6222 to extract the first member, op2ndb 6224 for an alternate version, and op2nd 7981 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 6221	. . 3 ⊢ ran {⟨𝐴, 𝐵⟩} = {𝐵}
3	2	unieqi 4921	. 2 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = ∪ {𝐵}
4		cnvsn.2	. . 3 ⊢ 𝐵 ∈ V
5	4	unisn 4930	. 2 ⊢ ∪ {𝐵} = 𝐵
6	3, 5	eqtri 2761	1 ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵

Syntax hints:   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4628  ⟨cop 4634  ∪ cuni 4908  ran crn 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  elxp4  7910  elxp5  7911  op2nd  7981  fo2nd  7993  f2ndres  7997  ixpsnf1o  8929  xpassen  9063  xpdom2  9064