Theorem tpss

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Hypotheses	tpss.1	|- A e. _V
	tpss.2	|- B e. _V
	tpss.3	|- C e. _V
Assertion	tpss	|- ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D )

Proof

Step	Hyp	Ref	Expression
1		tpss.1	|- A e. _V
2		tpss.2	|- B e. _V
3		tpss.3	|- C e. _V
4		unss	|- ( ( { A , B } C_ D /\ { C } C_ D ) <-> ( { A , B } u. { C } ) C_ D )
5		df-3an	|- ( ( A e. D /\ B e. D /\ C e. D ) <-> ( ( A e. D /\ B e. D ) /\ C e. D ) )
6	1 2	prss	|- ( ( A e. D /\ B e. D ) <-> { A , B } C_ D )
7	3	snss	|- ( C e. D <-> { C } C_ D )
8	6 7	anbi12i	|- ( ( ( A e. D /\ B e. D ) /\ C e. D ) <-> ( { A , B } C_ D /\ { C } C_ D ) )
9	5 8	bitri	|- ( ( A e. D /\ B e. D /\ C e. D ) <-> ( { A , B } C_ D /\ { C } C_ D ) )
10		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
11	10	sseq1i	|- ( { A , B , C } C_ D <-> ( { A , B } u. { C } ) C_ D )
12	4 9 11	3bitr4i	|- ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D )