Metamath Proof Explorer

Theorem prid1g

Description: An unordered pair contains its first member. Part of Theorem 7.6 of Quine p. 49. (Contributed by Stefan Allan, 8-Nov-2008)

Ref Expression
Assertion prid1g 
|- ( A e. V -> A e. { A , B } )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 1 orci 
 |-  ( A = A \/ A = B )
3 elprg 
 |-  ( A e. V -> ( A e. { A , B } <-> ( A = A \/ A = B ) ) )
4 2 3 mpbiri 
 |-  ( A e. V -> A e. { A , B } )