Theorem ex-id

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

	Ref	Expression
Assertion	ex-id	⊢ ( 5 I 5 ∧ ¬ 4 I 5 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 5 = 5
2		5re	⊢ 5 ∈ ℝ
3	2	elexi	⊢ 5 ∈ V
4	3	ideq	⊢ ( 5 I 5 ↔ 5 = 5 )
5	1 4	mpbir	⊢ 5 I 5
6		4re	⊢ 4 ∈ ℝ
7		4lt5	⊢ 4 < 5
8	6 7	ltneii	⊢ 4 ≠ 5
9	3	ideq	⊢ ( 4 I 5 ↔ 4 = 5 )
10	8 9	nemtbir	⊢ ¬ 4 I 5
11	5 10	pm3.2i	⊢ ( 5 I 5 ∧ ¬ 4 I 5 )