Metamath Proof Explorer


Theorem elrid

Description: Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022) (Proof shortened by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elrid
|- ( A e. ( _I |` X ) <-> E. x e. X A = <. x , x >. )

Proof

Step Hyp Ref Expression
1 df-res
 |-  ( _I |` X ) = ( _I i^i ( X X. _V ) )
2 1 eleq2i
 |-  ( A e. ( _I |` X ) <-> A e. ( _I i^i ( X X. _V ) ) )
3 elidinxp
 |-  ( A e. ( _I i^i ( X X. _V ) ) <-> E. x e. ( X i^i _V ) A = <. x , x >. )
4 inv1
 |-  ( X i^i _V ) = X
5 4 rexeqi
 |-  ( E. x e. ( X i^i _V ) A = <. x , x >. <-> E. x e. X A = <. x , x >. )
6 2 3 5 3bitri
 |-  ( A e. ( _I |` X ) <-> E. x e. X A = <. x , x >. )