Theorem op1sta 6228

Description: Extract the first member of an ordered pair. (See op2nda 6231 to extract the second member, op1stb 5455 for an alternate version, and op1st 8000 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 6219	. . 3 ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}
3	2	unieqi 4886	. 2 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = ∪ {𝐴}
4		cnvsn.1	. . 3 ⊢ 𝐴 ∈ V
5	4	unisn 4893	. 2 ⊢ ∪ {𝐴} = 𝐴
6	3, 5	eqtri 2788	1 ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457  {csn 4591  ⟨cop 4597  ∪ cuni 4874  dom cdm 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673

This theorem is used by:  elxp4  7925  op1st  8000  fo1st  8012  f1stres  8016  xpassen  9066  xpdom2  9067