Theorem resiexg 7934

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962   I cid 5581   × cxp 5686   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-res 5700

This theorem is referenced by:  ordiso  9553  wdomref  9609  dfac9  10174  relexp0g  15057  relexpsucnnr  15060  ndxarg  17229  idfu2nd  17927  idfu1st  17929  idfucl  17931  funcestrcsetclem4  18198  equivestrcsetc  18207  funcsetcestrclem4  18213  sursubmefmnd  18921  injsubmefmnd  18922  smndex1n0mnd  18937  islinds2  21850  pf1ind  22374  ausgrusgrb  29196  upgrres1lem1  29340  cusgrexilem1  29470  sizusglecusg  29495  pliguhgr  30514  bj-evalid  37058  bj-diagval  37156  poimirlem15  37621  xrnidresex  38388  dib0  41146  dicn0  41174  cdlemn11a  41189  dihord6apre  41238  dihatlat  41316  dihpN  41318  eldioph2lem1  42747  eldioph2lem2  42748  dfrtrcl5  43618  dfrcl2  43663  relexpiidm  43693  ushggricedg  47833  uspgrsprfo  47991  rngcidALTV  48117  ringcidALTV  48151