Theorem prid2

Description: An unordered pair contains its second member. Part of Theorem 7.6 of Quine p. 49. (Note: the proof from prid2g and ax-mp has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993)

	Ref	Expression
Hypothesis	prid2.1	$$⊢B\in \mathrm{V}$$
Assertion	prid2	$$⊢B\in \left\{A,B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		prid2.1	$$⊢B\in \mathrm{V}$$
2	1	prid1	$$⊢B\in \left\{B,A\right\}$$
3		prcom	$$⊢\left\{B,A\right\}=\left\{A,B\right\}$$
4	2 3	eleqtri	$$⊢B\in \left\{A,B\right\}$$