Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg ). (Contributed by NM, 13-Jan-2007) (Proof shortened by Peter Mazsa, 2-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | resiexg | |- ( A e. V -> ( _I |` A ) e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idssxp | |- ( _I |` A ) C_ ( A X. A ) |
|
| 2 | sqxpexg | |- ( A e. V -> ( A X. A ) e. _V ) |
|
| 3 | ssexg | |- ( ( ( _I |` A ) C_ ( A X. A ) /\ ( A X. A ) e. _V ) -> ( _I |` A ) e. _V ) |
|
| 4 | 1 2 3 | sylancr | |- ( A e. V -> ( _I |` A ) e. _V ) |