Metamath Proof Explorer


Theorem bj-diagval2

Description: Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the diagonal function, whereas bj-diagval views it as the functionalized identity. See df-bj-diag for the terminology. (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion bj-diagval2 Could not format assertion : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bj-diagval Could not format ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) with typecode |-
2 idinxpresid I A × A = I A
3 1 2 eqtr4di Could not format ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) with typecode |-