![]() |
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 7218). (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 6047 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | |
2 | sqxpexg 7744 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
3 | ssexg 5322 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
4 | 1, 2, 3 | sylancr 585 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2104 Vcvv 3472 ⊆ wss 3947 I cid 5572 × cxp 5673 ↾ cres 5677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-res 5687 |
This theorem is referenced by: ordiso 9513 wdomref 9569 dfac9 10133 relexp0g 14973 relexpsucnnr 14976 ndxarg 17133 idfu2nd 17831 idfu1st 17833 idfucl 17835 funcestrcsetclem4 18099 equivestrcsetc 18108 funcsetcestrclem4 18114 sursubmefmnd 18813 injsubmefmnd 18814 smndex1n0mnd 18829 islinds2 21587 pf1ind 22094 ausgrusgrb 28692 upgrres1lem1 28833 cusgrexilem1 28963 sizusglecusg 28987 pliguhgr 30006 bj-evalid 36260 bj-diagval 36358 poimirlem15 36806 xrnidresex 37580 dib0 40338 dicn0 40366 cdlemn11a 40381 dihord6apre 40430 dihatlat 40508 dihpN 40510 eldioph2lem1 41800 eldioph2lem2 41801 dfrtrcl5 42682 dfrcl2 42727 relexpiidm 42757 uspgrsprfo 46824 rngcidALTV 46977 ringcidALTV 47040 |
Copyright terms: Public domain | W3C validator |