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

Metamath Proof Explorer

Theorem prid2

Description: An unordered pair contains its second member. Part of Theorem 7.6 of Quine p. 49. (Note: the proof from prid2g and ax-mp has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993)

Ref Expression
Hypothesis prid2.1 
|- B e. _V
Assertion prid2 
|- B e. { A , B }

Proof

Step Hyp Ref Expression
1 prid2.1 
 |-  B e. _V
2 1 prid1 
 |-  B e. { B , A }
3 prcom 
 |-  { B , A } = { A , B }
4 2 3 eleqtri 
 |-  B e. { A , B }