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 6008	. 2 ⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
2		sqxpexg 7702	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
3		ssexg 5254	. 2 ⊢ ((( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ V) → ( I ↾ 𝐴) ∈ V)
4	1, 2, 3	sylancr 594	1 ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885   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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-id 5516  df-xp 5627  df-rel 5628  df-res 5633

This theorem is referenced by:  ordiso  9425  wdomref  9481  dfac9  10054  relexp0g  14979  relexpsucnnr  14982  ndxarg  17161  idfu2nd  17839  idfu1st  17841  idfucl  17843  funcestrcsetclem4  18104  equivestrcsetc  18113  funcsetcestrclem4  18119  sursubmefmnd  18859  injsubmefmnd  18860  smndex1n0mnd  18878  islinds2  21792  pf1ind  22345  ausgrusgrb  29256  upgrres1lem1  29400  cusgrexilem1  29530  sizusglecusg  29554  pliguhgr  30579  bj-evalid  37449  bj-diagval  37549  poimirlem15  38017  xrnidresex  38812  dib0  41671  dicn0  41699  cdlemn11a  41714  dihord6apre  41763  dihatlat  41841  dihpN  41843  eldioph2lem1  43224  eldioph2lem2  43225  dfrtrcl5  44088  dfrcl2  44133  relexpiidm  44163  ushggricedg  48432  uspgrsprfo  48653  rngcidALTV  48779  ringcidALTV  48813  resipos  49479  cofidvala  49620  cofidval  49623  opf2fval  49909  fucoppc  49914  idfudiag1bas  50028  idfudiag1  50029