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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prid1g | |
|
2 | prcom | |
|
3 | 1 2 | eleqtrdi | |