Metamath Proof Explorer

Theorem prid2g

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

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

Proof

Step Hyp Ref Expression
1 prid1g 
 |-  ( B e. V -> B e. { B , A } )
2 prcom 
 |-  { B , A } = { A , B }
3 1 2 eleqtrdi 
 |-  ( B e. V -> B e. { A , B } )