Metamath Proof Explorer

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 
 |-  (/) e. _V
2 1 snid 
 |-  (/) e. { (/) }
3 snex 
 |-  { (/) } e. _V
4 3 epeli 
 |-  ( (/) _E { (/) } <-> (/) e. { (/) } )
5 2 4 mpbir 
 |-  (/) _E { (/) }