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\in V\to A\in \left\{A,B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2	1	orci	$$⊢\left(A=A\vee A=B\right)$$
3		elprg	$$⊢A\in V\to \left(A\in \left\{A,B\right\}\leftrightarrow \left(A=A\vee A=B\right)\right)$$
4	2 3	mpbiri	$$⊢A\in V\to A\in \left\{A,B\right\}$$