Metamath Proof Explorer

Theorem prid1g

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

Ref Expression
Assertion prid1g A V A A B


Step Hyp Ref Expression
1 eqid A = A
2 1 orci A = A A = B
3 elprg A V A A B A = A A = B
4 2 3 mpbiri A V A A B