Description: Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 after elrid . (Contributed by BJ, 28-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elid | |- ( A e. _I <-> E. x A = <. x , x >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reli | |- Rel _I |
|
| 2 | dfrel3 | |- ( Rel _I <-> ( _I |` _V ) = _I ) |
|
| 3 | 1 2 | mpbi | |- ( _I |` _V ) = _I |
| 4 | 3 | eqcomi | |- _I = ( _I |` _V ) |
| 5 | 4 | eleq2i | |- ( A e. _I <-> A e. ( _I |` _V ) ) |
| 6 | elrid | |- ( A e. ( _I |` _V ) <-> E. x e. _V A = <. x , x >. ) |
|
| 7 | rexv | |- ( E. x e. _V A = <. x , x >. <-> E. x A = <. x , x >. ) |
|
| 8 | 5 6 7 | 3bitri | |- ( A e. _I <-> E. x A = <. x , x >. ) |