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	⊢ { ∅ , 𝐴 } ∈ Moore

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		0ss	⊢ ∅ ⊆ 𝐴
3		bj-prmoore	⊢ ( ( ∅ ∈ V ∧ ∅ ⊆ 𝐴 ) → { ∅ , 𝐴 } ∈ Moore )
4	1 2 3	mp2an	⊢ { ∅ , 𝐴 } ∈ Moore