Metamath Proof Explorer


Theorem opi1

Description: One of the two elements in an ordered pair. (Contributed by NM, 15-Jul-1993) (Revised by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

Ref Expression
Hypotheses opi1.1
|- A e. _V
opi1.2
|- B e. _V
Assertion opi1
|- { A } e. <. A , B >.

Proof

Step Hyp Ref Expression
1 opi1.1
 |-  A e. _V
2 opi1.2
 |-  B e. _V
3 snex
 |-  { A } e. _V
4 3 prid1
 |-  { A } e. { { A } , { A , B } }
5 1 2 dfop
 |-  <. A , B >. = { { A } , { A , B } }
6 4 5 eleqtrri
 |-  { A } e. <. A , B >.