Metamath Proof Explorer

Theorem ididg

Description: A set is identical to itself. (Contributed by NM, 28-May-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ididg 
|- ( A e. V -> A _I A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 ideqg 
 |-  ( A e. V -> ( A _I A <-> A = A ) )
3 1 2 mpbiri 
 |-  ( A e. V -> A _I A )