Theorem resiexg 7907

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904   I cid 5554   × cxp 5658   ↾ cres 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-id 5555  df-xp 5666  df-rel 5667  df-res 5672

This theorem is used by:  ordiso  9476  wdomref  9532  dfac9  10127  relexp0g  15066  relexpsucnnr  15069  ndxarg  17262  idfu2nd  17940  idfu1st  17942  idfucl  17944  funcestrcsetclem4  18205  equivestrcsetc  18214  funcsetcestrclem4  18220  sursubmefmnd  18961  injsubmefmnd  18962  smndex1n0mnd  18980  islinds2  21974  pf1ind  22526  ausgrusgrb  29526  upgrres1lem1  29670  cusgrexilem1  29800  sizusglecusg  29824  pliguhgr  30849  bj-evalid  37746  bj-diagval  37846  poimirlem15  38314  xrnidresex  39107  dib0  41966  dicn0  41994  cdlemn11a  42009  dihord6apre  42058  dihatlat  42136  dihpN  42138  eldioph2lem1  43519  eldioph2lem2  43520  dfrtrcl5  44383  dfrcl2  44428  relexpiidm  44458  ushggricedg  48720  uspgrsprfo  48941  rngcidALTV  49067  ringcidALTV  49101  resipos  49781  cofidvala  49922  cofidval  49925  opf2fval  50211  fucoppc  50216  idfudiag1bas  50330  idfudiag1  50331