Theorem resiexg 7895

Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7201). (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 6040	. 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
2		sqxpexg 7740	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
3		ssexg 5281	. 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V)
4	1, 2, 3	sylancr 596	1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906   I cid 5543   × cxp 5647   ↾ cres 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pow 5324  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-id 5544  df-xp 5655  df-rel 5656  df-res 5661

This theorem is referenced by:  ordiso  9466  wdomref  9522  dfac9  10095  relexp0g  15037  relexpsucnnr  15040  ndxarg  17234  idfu2nd  17912  idfu1st  17914  idfucl  17916  funcestrcsetclem4  18177  equivestrcsetc  18186  funcsetcestrclem4  18192  sursubmefmnd  18932  injsubmefmnd  18933  smndex1n0mnd  18951  islinds2  21867  pf1ind  22420  ausgrusgrb  29368  upgrres1lem1  29512  cusgrexilem1  29642  sizusglecusg  29666  pliguhgr  30691  bj-evalid  37571  bj-diagval  37671  poimirlem15  38139  xrnidresex  38934  dib0  41793  dicn0  41821  cdlemn11a  41836  dihord6apre  41885  dihatlat  41963  dihpN  41965  eldioph2lem1  43346  eldioph2lem2  43347  dfrtrcl5  44210  dfrcl2  44255  relexpiidm  44285  ushggricedg  48554  uspgrsprfo  48775  rngcidALTV  48901  ringcidALTV  48935  resipos  49601  cofidvala  49742  cofidval  49745  opf2fval  50031  fucoppc  50036  idfudiag1bas  50150  idfudiag1  50151