Theorem resiexg 7851

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438   ⊆ wss 3899   I cid 5515   × cxp 5619   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-res 5633

This theorem is referenced by:  ordiso  9412  wdomref  9468  dfac9  10038  relexp0g  14939  relexpsucnnr  14942  ndxarg  17117  idfu2nd  17794  idfu1st  17796  idfucl  17798  funcestrcsetclem4  18059  equivestrcsetc  18068  funcsetcestrclem4  18074  sursubmefmnd  18814  injsubmefmnd  18815  smndex1n0mnd  18830  islinds2  21760  pf1ind  22280  ausgrusgrb  29154  upgrres1lem1  29298  cusgrexilem1  29428  sizusglecusg  29453  pliguhgr  30477  bj-evalid  37131  bj-diagval  37229  poimirlem15  37685  xrnidresex  38464  dib0  41273  dicn0  41301  cdlemn11a  41316  dihord6apre  41365  dihatlat  41443  dihpN  41445  eldioph2lem1  42867  eldioph2lem2  42868  dfrtrcl5  43736  dfrcl2  43781  relexpiidm  43811  ushggricedg  48041  uspgrsprfo  48262  rngcidALTV  48388  ringcidALTV  48422  resipos  49089  cofidvala  49231  cofidval  49234  opf2fval  49520  fucoppc  49525  idfudiag1bas  49639  idfudiag1  49640