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

Metamath Proof Explorer

Theorem op1st

Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004)

Ref Expression
Hypotheses op1st.1 ⊢ A ∈ V
op1st.2 ⊢ B ∈ V
Assertion op1st ⊢ 1 st ⁡ A B = A

Proof

Step Hyp Ref Expression
1 op1st.1 ⊢ A ∈ V
2 op1st.2 ⊢ B ∈ V
3 1stval ⊢ 1 st ⁡ A B = ⋃ dom ⁡ A B
4 1 2 op1sta ⊢ ⋃ dom ⁡ A B = A
5 3 4 eqtri ⊢ 1 st ⁡ A B = A