![]() |
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 7161). (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 6000 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | |
2 | sqxpexg 7681 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
3 | ssexg 5278 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
4 | 1, 2, 3 | sylancr 587 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Vcvv 3443 ⊆ wss 3908 I cid 5528 × cxp 5629 ↾ cres 5633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7664 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-id 5529 df-xp 5637 df-rel 5638 df-res 5643 |
This theorem is referenced by: ordiso 9410 wdomref 9466 dfac9 10030 relexp0g 14861 relexpsucnnr 14864 ndxarg 17022 idfu2nd 17717 idfu1st 17719 idfucl 17721 funcestrcsetclem4 17985 equivestrcsetc 17994 funcsetcestrclem4 18000 sursubmefmnd 18660 injsubmefmnd 18661 smndex1n0mnd 18676 islinds2 21166 pf1ind 21667 ausgrusgrb 27961 upgrres1lem1 28102 cusgrexilem1 28232 sizusglecusg 28256 pliguhgr 29273 bj-evalid 35479 bj-diagval 35577 poimirlem15 36025 xrnidresex 36801 dib0 39559 dicn0 39587 cdlemn11a 39602 dihord6apre 39651 dihatlat 39729 dihpN 39731 eldioph2lem1 40986 eldioph2lem2 40987 dfrtrcl5 41806 dfrcl2 41851 relexpiidm 41881 uspgrsprfo 45945 rngcidALTV 46184 ringcidALTV 46247 |
Copyright terms: Public domain | W3C validator |