Theorem tpnzd

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

	Ref	Expression
Hypothesis	tpnzd.1	$$⊢\phi \to A\in V$$
Assertion	tpnzd	$$⊢\phi \to \left\{A,B,C\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		tpnzd.1	$$⊢\phi \to A\in V$$
2		tpid1g	$$⊢A\in V\to A\in \left\{A,B,C\right\}$$
3		ne0i	$$⊢A\in \left\{A,B,C\right\}\to \left\{A,B,C\right\}\ne \varnothing$$
4	1 2 3	3syl	$$⊢\phi \to \left\{A,B,C\right\}\ne \varnothing$$