Theorem dfpr2

Description: Alternate definition of unordered pair. Definition 5.1 of TakeutiZaring p. 15. (Contributed by NM, 24-Apr-1994)

	Ref	Expression
Assertion	dfpr2	$$⊢\left\{A,B\right\}=\left\{x|\left(x=A\vee x=B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
2		elun	$$⊢x\in \left(\left\{A\right\}\cup \left\{B\right\}\right)\leftrightarrow \left(x\in \left\{A\right\}\vee x\in \left\{B\right\}\right)$$
3		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
4		velsn	$$⊢x\in \left\{B\right\}\leftrightarrow x=B$$
5	3 4	orbi12i	$$⊢\left(x\in \left\{A\right\}\vee x\in \left\{B\right\}\right)\leftrightarrow \left(x=A\vee x=B\right)$$
6	2 5	bitri	$$⊢x\in \left(\left\{A\right\}\cup \left\{B\right\}\right)\leftrightarrow \left(x=A\vee x=B\right)$$
7	6	abbi2i	$$⊢\left\{A\right\}\cup \left\{B\right\}=\left\{x|\left(x=A\vee x=B\right)\right\}$$
8	1 7	eqtri	$$⊢\left\{A,B\right\}=\left\{x|\left(x=A\vee x=B\right)\right\}$$