Theorem resiexg 7952

Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7252). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)

Assertion

Ref	Expression
resiexg	⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)

Proof of Theorem resiexg

Step	Hyp	Ref	Expression
1		idssxp 6078	. 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
2		sqxpexg 7790	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
3		ssexg 5341	. 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V)
4	1, 2, 3	sylancr 586	1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976   I cid 5592   × cxp 5698   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-res 5712

This theorem is referenced by:  ordiso  9585  wdomref  9641  dfac9  10206  relexp0g  15071  relexpsucnnr  15074  ndxarg  17243  idfu2nd  17941  idfu1st  17943  idfucl  17945  funcestrcsetclem4  18212  equivestrcsetc  18221  funcsetcestrclem4  18227  sursubmefmnd  18931  injsubmefmnd  18932  smndex1n0mnd  18947  islinds2  21856  pf1ind  22380  ausgrusgrb  29200  upgrres1lem1  29344  cusgrexilem1  29474  sizusglecusg  29499  pliguhgr  30518  bj-evalid  37042  bj-diagval  37140  poimirlem15  37595  xrnidresex  38363  dib0  41121  dicn0  41149  cdlemn11a  41164  dihord6apre  41213  dihatlat  41291  dihpN  41293  eldioph2lem1  42716  eldioph2lem2  42717  dfrtrcl5  43591  dfrcl2  43636  relexpiidm  43666  ushggricedg  47780  uspgrsprfo  47871  rngcidALTV  47997  ringcidALTV  48031