Theorem resiexg 7856

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902   I cid 5519   × cxp 5623   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5520  df-xp 5631  df-rel 5632  df-res 5637

This theorem is referenced by:  ordiso  9425  wdomref  9481  dfac9  10051  relexp0g  14949  relexpsucnnr  14952  ndxarg  17127  idfu2nd  17805  idfu1st  17807  idfucl  17809  funcestrcsetclem4  18070  equivestrcsetc  18079  funcsetcestrclem4  18085  sursubmefmnd  18825  injsubmefmnd  18826  smndex1n0mnd  18841  islinds2  21772  pf1ind  22303  ausgrusgrb  29242  upgrres1lem1  29386  cusgrexilem1  29516  sizusglecusg  29541  pliguhgr  30565  bj-evalid  37283  bj-diagval  37381  poimirlem15  37838  xrnidresex  38633  dib0  41492  dicn0  41520  cdlemn11a  41535  dihord6apre  41584  dihatlat  41662  dihpN  41664  eldioph2lem1  43069  eldioph2lem2  43070  dfrtrcl5  43937  dfrcl2  43982  relexpiidm  44012  ushggricedg  48240  uspgrsprfo  48461  rngcidALTV  48587  ringcidALTV  48621  resipos  49287  cofidvala  49428  cofidval  49431  opf2fval  49717  fucoppc  49722  idfudiag1bas  49836  idfudiag1  49837