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	|- { A , B , C } = { x | ( x = A \/ x = B \/ x = C ) }

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	eltp	|- ( x e. { A , B , C } <-> ( x = A \/ x = B \/ x = C ) )
3	2	eqabi	|- { A , B , C } = { x | ( x = A \/ x = B \/ x = C ) }