Theorem op1sta 6181

Description: Extract the first member of an ordered pair. (See op2nda 6184 to extract the second member, op1stb 5417 for an alternate version, and op1st 7939 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)

Hypotheses

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

Assertion

Ref	Expression
op1sta	⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴

Proof of Theorem op1sta

Step	Hyp	Ref	Expression
1		cnvsn.2	. . . 4 ⊢ 𝐵 ∈ V
2	1	dmsnop 6172	. . 3 ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}
3	2	unieqi 4873	. 2 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = ∪ {𝐴}
4		cnvsn.1	. . 3 ⊢ 𝐴 ∈ V
5	4	unisn 4880	. 2 ⊢ ∪ {𝐴} = 𝐴
6	3, 5	eqtri 2757	1 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4578  ⟨cop 4584  ∪ cuni 4861  dom cdm 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-dm 5632

This theorem is referenced by:  elxp4  7862  op1st  7939  fo1st  7951  f1stres  7955  xpassen  8997  xpdom2  8998