Theorem tpnz

Description: An unordered triple containing a set is not empty. (Contributed by NM, 10-Apr-1994)

	Ref	Expression
Hypothesis	tpnz.1	⊢ 𝐴 ∈ V
Assertion	tpnz	⊢ { 𝐴 , 𝐵 , 𝐶 } ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		tpnz.1	⊢ 𝐴 ∈ V
2	1	tpid1	⊢ 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 }
3	2	ne0ii	⊢ { 𝐴 , 𝐵 , 𝐶 } ≠ ∅