Theorem tpnzd

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

	Ref	Expression
Hypothesis	tpnzd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	tpnzd	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		tpnzd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		tpid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
3		ne0i	⊢ ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )
4	1 2 3	3syl	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )