Theorem prnzg

Description: A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	prnzg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 , 𝐵 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		prid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
2	1	ne0d	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 , 𝐵 } ≠ ∅ )