Theorem resiexg 7868

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911   I cid 5525   × cxp 5629   ↾ cres 5633

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  ordiso  9445  wdomref  9501  dfac9  10066  relexp0g  14964  relexpsucnnr  14967  ndxarg  17142  idfu2nd  17819  idfu1st  17821  idfucl  17823  funcestrcsetclem4  18084  equivestrcsetc  18093  funcsetcestrclem4  18099  sursubmefmnd  18805  injsubmefmnd  18806  smndex1n0mnd  18821  islinds2  21755  pf1ind  22275  ausgrusgrb  29145  upgrres1lem1  29289  cusgrexilem1  29419  sizusglecusg  29444  pliguhgr  30465  bj-evalid  37057  bj-diagval  37155  poimirlem15  37622  xrnidresex  38386  dib0  41151  dicn0  41179  cdlemn11a  41194  dihord6apre  41243  dihatlat  41321  dihpN  41323  eldioph2lem1  42741  eldioph2lem2  42742  dfrtrcl5  43611  dfrcl2  43656  relexpiidm  43686  ushggricedg  47920  uspgrsprfo  48129  rngcidALTV  48255  ringcidALTV  48289  resipos  48956  cofidvala  49098  cofidval  49101  opf2fval  49387  fucoppc  49392  idfudiag1bas  49506  idfudiag1  49507