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 7009). (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 5901 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | |
2 | sqxpexg 7518 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
3 | ssexg 5201 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
4 | 1, 2, 3 | sylancr 590 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 Vcvv 3398 ⊆ wss 3853 I cid 5439 × cxp 5534 ↾ cres 5538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-opab 5102 df-id 5440 df-xp 5542 df-rel 5543 df-res 5548 |
This theorem is referenced by: ordiso 9110 wdomref 9166 dfac9 9715 relexp0g 14550 relexpsucnnr 14553 ndxarg 16690 idfu2nd 17337 idfu1st 17339 idfucl 17341 funcestrcsetclem4 17604 equivestrcsetc 17613 funcsetcestrclem4 17619 sursubmefmnd 18277 injsubmefmnd 18278 smndex1n0mnd 18293 islinds2 20729 pf1ind 21225 ausgrusgrb 27210 upgrres1lem1 27351 cusgrexilem1 27481 sizusglecusg 27505 pliguhgr 28521 bj-evalid 34931 bj-diagval 35029 poimirlem15 35478 xrnidresex 36219 dib0 38864 dicn0 38892 cdlemn11a 38907 dihord6apre 38956 dihatlat 39034 dihpN 39036 eldioph2lem1 40226 eldioph2lem2 40227 dfrtrcl5 40854 dfrcl2 40900 relexpiidm 40930 uspgrsprfo 44926 rngcidALTV 45165 ringcidALTV 45228 |
Copyright terms: Public domain | W3C validator |