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 6981). (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 5919 | . 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | |
2 | sqxpexg 7480 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | |
3 | ssexg 5230 | . 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V) | |
4 | 1, 2, 3 | sylancr 589 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 Vcvv 3497 ⊆ wss 3939 I cid 5462 × cxp 5556 ↾ cres 5560 |
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 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-opab 5132 df-id 5463 df-xp 5564 df-rel 5565 df-res 5570 |
This theorem is referenced by: ordiso 8983 wdomref 9039 dfac9 9565 relexp0g 14384 relexpsucnnr 14387 ndxarg 16511 idfu2nd 17150 idfu1st 17152 idfucl 17154 funcestrcsetclem4 17396 equivestrcsetc 17405 funcsetcestrclem4 17411 sursubmefmnd 18064 injsubmefmnd 18065 smndex1n0mnd 18080 pf1ind 20521 islinds2 20960 ausgrusgrb 26953 upgrres1lem1 27094 cusgrexilem1 27224 sizusglecusg 27248 pliguhgr 28266 bj-evalid 34371 bj-diagval 34470 poimirlem15 34911 xrnidresex 35659 dib0 38304 dicn0 38332 cdlemn11a 38347 dihord6apre 38396 dihatlat 38474 dihpN 38476 eldioph2lem1 39363 eldioph2lem2 39364 dfrtrcl5 39995 dfrcl2 40025 relexpiidm 40055 uspgrsprfo 44030 rngcidALTV 44269 ringcidALTV 44332 |
Copyright terms: Public domain | W3C validator |