Theorem resiexg 7908

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899   I cid 5542   × cxp 5646   ↾ cres 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5543  df-xp 5654  df-rel 5655  df-res 5660

This theorem is used by:  ordiso  9488  wdomref  9544  dfac9  10172  relexp0g  15128  relexpsucnnr  15131  ndxarg  17321  idfu2nd  17999  idfu1st  18001  idfucl  18003  funcestrcsetclem4  18264  equivestrcsetc  18273  funcsetcestrclem4  18279  sursubmefmnd  19039  injsubmefmnd  19040  smndex1n0mnd  19058  islinds2  22066  pf1ind  22620  ausgrusgrb  29665  upgrres1lem1  29809  cusgrexilem1  29939  sizusglecusg  29963  pliguhgr  31007  bj-evalid  37911  bj-diagval  38009  poimirlem15  38467  xrnidresex  39276  dib0  42135  dicn0  42163  cdlemn11a  42178  dihord6apre  42227  dihatlat  42305  dihpN  42307  eldioph2lem1  43703  eldioph2lem2  43704  dfrtrcl5  44567  dfrcl2  44612  relexpiidm  44642  ushggricedg  48941  uspgrsprfo  49162  rngcidALTV  49287  ringcidALTV  49321  resipos  49999  cofidvala  50140  cofidval  50143  opf2fval  50429  fucoppc  50434  idfudiag1bas  50548  idfudiag1  50549