This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \land \neg 4 I 5)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ 5 = 5$
2		5re	$⊢ 5 \in ℝ$
3	2	elexi	$⊢ 5 \in V$
4	3	ideq	$⊢ 5 I 5 \leftrightarrow 5 = 5$
5	1 4	mpbir	$⊢ 5 I 5$
6		4re	$⊢ 4 \in ℝ$
7		4lt5	$⊢ 4 < 5$
8	6 7	ltneii	$⊢ 4 \neq 5$
9	3	ideq	$⊢ 4 I 5 \leftrightarrow 4 = 5$
10	8 9	nemtbir	$⊢ \neg 4 I 5$
11	5 10	pm3.2i	$⊢ (5 I 5 \land \neg 4 I 5)$