Theorem 0sn0ep

Description: An example for the membership relation. (Contributed by AV, 19-Jun-2022)

	Ref	Expression
Assertion	0sn0ep	⊢ ∅ E { ∅ }

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	snid	⊢ ∅ ∈ { ∅ }
3		snex	⊢ { ∅ } ∈ V
4	3	epeli	⊢ ( ∅ E { ∅ } ↔ ∅ ∈ { ∅ } )
5	2 4	mpbir	⊢ ∅ E { ∅ }