Theorem dftp2

Description: Alternate definition of unordered triple of classes. Special case of Definition 5.3 of TakeutiZaring p. 16. (Contributed by NM, 8-Apr-1994)

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

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	eltp	$$⊢x\in \left\{A,B,C\right\}\leftrightarrow \left(x=A\vee x=B\vee x=C\right)$$
3	2	eqabi	$$⊢\left\{A,B,C\right\}=\left\{x|\left(x=A\vee x=B\vee x=C\right)\right\}$$