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 ∈ ℕ
2	1	elexi	⊢ 5 ∈ V
3	2	prid2	⊢ 5 ∈ { 1 , 5 }
4		prex	⊢ { 1 , 5 } ∈ V
5	4	epeli	⊢ ( 5 E { 1 , 5 } ↔ 5 ∈ { 1 , 5 } )
6	3 5	mpbir	⊢ 5 E { 1 , 5 }