Metamath Proof Explorer

Theorem ex-eprel

Description: Example for df-eprel . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion ex-eprel 
|- 5 _E { 1 , 5 }

Proof

Step Hyp Ref Expression
1 5nn 
 |-  5 e. NN
2 1 elexi 
 |-  5 e. _V
3 2 prid2 
 |-  5 e. { 1 , 5 }
4 prex 
 |-  { 1 , 5 } e. _V
5 4 epeli 
 |-  ( 5 _E { 1 , 5 } <-> 5 e. { 1 , 5 } )
6 3 5 mpbir 
 |-  5 _E { 1 , 5 }