Theorem resiexg 7909

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911   I cid 5556   × cxp 5660   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-id 5557  df-xp 5668  df-rel 5669  df-res 5674

This theorem is referenced by:  ordiso  9478  wdomref  9534  dfac9  10120  relexp0g  15059  relexpsucnnr  15062  ndxarg  17256  idfu2nd  17934  idfu1st  17936  idfucl  17938  funcestrcsetclem4  18199  equivestrcsetc  18208  funcsetcestrclem4  18214  sursubmefmnd  18955  injsubmefmnd  18956  smndex1n0mnd  18974  islinds2  21932  pf1ind  22484  ausgrusgrb  29456  upgrres1lem1  29600  cusgrexilem1  29730  sizusglecusg  29754  pliguhgr  30779  bj-evalid  37641  bj-diagval  37741  poimirlem15  38209  xrnidresex  39004  dib0  41863  dicn0  41891  cdlemn11a  41906  dihord6apre  41955  dihatlat  42033  dihpN  42035  eldioph2lem1  43418  eldioph2lem2  43419  dfrtrcl5  44282  dfrcl2  44327  relexpiidm  44357  ushggricedg  48616  uspgrsprfo  48837  rngcidALTV  48963  ringcidALTV  48997  resipos  49673  cofidvala  49814  cofidval  49817  opf2fval  50103  fucoppc  50108  idfudiag1bas  50222  idfudiag1  50223