Metamath Proof Explorer

Theorem prid1

Description: An unordered pair contains its first member. Part of Theorem 7.6 of Quine p. 49. (Contributed by NM, 24-Jun-1993)

Ref Expression
Hypothesis prid1.1 A V
Assertion prid1 A A B


Step Hyp Ref Expression
1 prid1.1 A V
2 prid1g A V A A B
3 1 2 ax-mp A A B