Metamath Proof Explorer

Theorem bj-0nmoore

Description: The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021)

Ref Expression
Assertion bj-0nmoore 
|- -. (/) e. Moore_

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. U. (/) e. (/)
2 bj-ismoored0 
 |-  ( (/) e. Moore_ -> U. (/) e. (/) )
3 1 2 mto 
 |-  -. (/) e. Moore_