This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem op1sta

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

	Ref	Expression
Hypotheses	cnvsn.1	⊢ 𝐴 ∈ V
	cnvsn.2	⊢ 𝐵 ∈ V
Assertion	op1sta	⊢ ∪ dom { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐴

Proof

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