Metamath Proof Explorer

Theorem bj-pr0moore

Description: A pair containing the empty set is a Moore collection. (Contributed by BJ, 4-Oct-2026)

Ref Expression
Assertion bj-pr0moore 
|- { (/) , A } e. Moore_

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 0ss 
 |-  (/) C_ A
3 bj-prmoore 
 |-  ( ( (/) e. _V /\ (/) C_ A ) -> { (/) , A } e. Moore_ )
4 1 2 3 mp2an 
 |-  { (/) , A } e. Moore_