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 BVBAB

Proof

Step Hyp Ref Expression
1 prid1g BVBBA
2 prcom BA=AB
3 1 2 eleqtrdi BVBAB