Theorem tpnzd

Description: An unordered triple containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019)

	Ref	Expression
Hypothesis	tpnzd.1	|- ( ph -> A e. V )
Assertion	tpnzd	|- ( ph -> { A , B , C } =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		tpnzd.1	|- ( ph -> A e. V )
2		tpid1g	|- ( A e. V -> A e. { A , B , C } )
3		ne0i	|- ( A e. { A , B , C } -> { A , B , C } =/= (/) )
4	1 2 3	3syl	|- ( ph -> { A , B , C } =/= (/) )