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 ( 𝐴𝑉𝐴 I 𝐴 )

Proof

Step Hyp Ref Expression
1 eqid 𝐴 = 𝐴
2 ideqg ( 𝐴𝑉 → ( 𝐴 I 𝐴𝐴 = 𝐴 ) )
3 1 2 mpbiri ( 𝐴𝑉𝐴 I 𝐴 )