Metamath Proof Explorer

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 
|- ( A e. V -> { A , B } =/= (/) )

Proof

Step Hyp Ref Expression
1 prid1g 
 |-  ( A e. V -> A e. { A , B } )
2 1 ne0d 
 |-  ( A e. V -> { A , B } =/= (/) )