Theorem resiexg 7908

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926   I cid 5547   × cxp 5652   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-res 5666

This theorem is referenced by:  ordiso  9530  wdomref  9586  dfac9  10151  relexp0g  15041  relexpsucnnr  15044  ndxarg  17215  idfu2nd  17890  idfu1st  17892  idfucl  17894  funcestrcsetclem4  18155  equivestrcsetc  18164  funcsetcestrclem4  18170  sursubmefmnd  18874  injsubmefmnd  18875  smndex1n0mnd  18890  islinds2  21773  pf1ind  22293  ausgrusgrb  29144  upgrres1lem1  29288  cusgrexilem1  29418  sizusglecusg  29443  pliguhgr  30467  bj-evalid  37094  bj-diagval  37192  poimirlem15  37659  xrnidresex  38425  dib0  41183  dicn0  41211  cdlemn11a  41226  dihord6apre  41275  dihatlat  41353  dihpN  41355  eldioph2lem1  42783  eldioph2lem2  42784  dfrtrcl5  43653  dfrcl2  43698  relexpiidm  43728  ushggricedg  47940  uspgrsprfo  48123  rngcidALTV  48249  ringcidALTV  48283  resipos  48949  idfudiag1bas  49409  idfudiag1  49410