Description: A pair containing a set is not empty. (Contributed by NM, 9Apr1994)
Ref  Expression  

Hypothesis  prnz.1   A e. _V 

Assertion  prnz   { A , B } =/= (/) 
Step  Hyp  Ref  Expression 

1  prnz.1   A e. _V 

2  1  prid1   A e. { A , B } 
3  2  ne0ii   { A , B } =/= (/) 