![]() |
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 6798). (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 5754 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | |
2 | sqxpexg 7288 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
3 | ssexg 5077 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
4 | 1, 2, 3 | sylancr 578 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2048 Vcvv 3409 ⊆ wss 3825 I cid 5304 × cxp 5398 ↾ cres 5402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-id 5305 df-xp 5406 df-rel 5407 df-res 5412 |
This theorem is referenced by: ordiso 8767 wdomref 8823 dfac9 9348 relexp0g 14232 relexpsucnnr 14235 ndxarg 16354 idfu2nd 16995 idfu1st 16997 idfucl 16999 funcestrcsetclem4 17241 equivestrcsetc 17250 funcsetcestrclem4 17256 pf1ind 20210 islinds2 20649 ausgrusgrb 26643 upgrres1lem1 26784 cusgrexilem1 26914 sizusglecusg 26938 pliguhgr 28030 bj-evalid 33811 poimirlem15 34296 xrnidresex 35048 dib0 37693 dicn0 37721 cdlemn11a 37736 dihord6apre 37785 dihatlat 37863 dihpN 37865 eldioph2lem1 38697 eldioph2lem2 38698 dfrtrcl5 39297 dfrcl2 39327 relexpiidm 39357 uspgrsprfo 43331 rngcidALTV 43566 ringcidALTV 43629 |
Copyright terms: Public domain | W3C validator |