![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resiexg | Structured version Visualization version GIF version |
Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7166). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
Ref | Expression |
---|---|
resiexg | ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idssxp 6003 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | |
2 | sqxpexg 7690 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
3 | ssexg 5281 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
4 | 1, 2, 3 | sylancr 588 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3444 ⊆ wss 3911 I cid 5531 × cxp 5632 ↾ cres 5636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-id 5532 df-xp 5640 df-rel 5641 df-res 5646 |
This theorem is referenced by: ordiso 9457 wdomref 9513 dfac9 10077 relexp0g 14913 relexpsucnnr 14916 ndxarg 17073 idfu2nd 17768 idfu1st 17770 idfucl 17772 funcestrcsetclem4 18036 equivestrcsetc 18045 funcsetcestrclem4 18051 sursubmefmnd 18711 injsubmefmnd 18712 smndex1n0mnd 18727 islinds2 21235 pf1ind 21737 ausgrusgrb 28158 upgrres1lem1 28299 cusgrexilem1 28429 sizusglecusg 28453 pliguhgr 29470 bj-evalid 35593 bj-diagval 35691 poimirlem15 36139 xrnidresex 36915 dib0 39673 dicn0 39701 cdlemn11a 39716 dihord6apre 39765 dihatlat 39843 dihpN 39845 eldioph2lem1 41126 eldioph2lem2 41127 dfrtrcl5 41989 dfrcl2 42034 relexpiidm 42064 uspgrsprfo 46136 rngcidALTV 46375 ringcidALTV 46438 |
Copyright terms: Public domain | W3C validator |