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 ⊢ A ∈ V
cnvsn.2 ⊢ B ∈ V
Assertion op1sta ⊢ ⋃ dom ⁡ A B = A

Proof

Step Hyp Ref Expression
1 cnvsn.1 ⊢ A ∈ V
2 cnvsn.2 ⊢ B ∈ V
3 2 dmsnop ⊢ dom ⁡ A B = A
4 3 unieqi ⊢ ⋃ dom ⁡ A B = ⋃ A
5 1 unisn ⊢ ⋃ A = A
6 4 5 eqtri ⊢ ⋃ dom ⁡ A B = A