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 /\ -. 4 _I 5 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  5 = 5
2 5re 
 |-  5 e. RR
3 2 elexi 
 |-  5 e. _V
4 3 ideq 
 |-  ( 5 _I 5 <-> 5 = 5 )
5 1 4 mpbir 
 |-  5 _I 5
6 4re 
 |-  4 e. RR
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 )