Theorem tpssg

Description: An ordered triplet of elements of a class is a subset of the class. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Assertion	tpssg	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D ) )

Proof

Step	Hyp	Ref	Expression
1		df-3an	|- ( ( A e. D /\ B e. D /\ C e. D ) <-> ( ( A e. D /\ B e. D ) /\ C e. D ) )
2		prssg	|- ( ( A e. V /\ B e. W ) -> ( ( A e. D /\ B e. D ) <-> { A , B } C_ D ) )
3		snssg	|- ( C e. X -> ( C e. D <-> { C } C_ D ) )
4	2 3	bi2anan9	|- ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( ( ( A e. D /\ B e. D ) /\ C e. D ) <-> ( { A , B } C_ D /\ { C } C_ D ) ) )
5		unss	|- ( ( { A , B } C_ D /\ { C } C_ D ) <-> ( { A , B } u. { C } ) C_ D )
6		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
7	6	sseq1i	|- ( { A , B , C } C_ D <-> ( { A , B } u. { C } ) C_ D )
8	5 7	bitr4i	|- ( ( { A , B } C_ D /\ { C } C_ D ) <-> { A , B , C } C_ D )
9	4 8	bitrdi	|- ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( ( ( A e. D /\ B e. D ) /\ C e. D ) <-> { A , B , C } C_ D ) )
10	1 9	bitrid	|- ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D ) )
11	10	3impa	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D ) )