Theorem resiexg 7845

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903   I cid 5513   × cxp 5617   ↾ cres 5621

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  ordiso  9408  wdomref  9464  dfac9  10031  relexp0g  14929  relexpsucnnr  14932  ndxarg  17107  idfu2nd  17784  idfu1st  17786  idfucl  17788  funcestrcsetclem4  18049  equivestrcsetc  18058  funcsetcestrclem4  18064  sursubmefmnd  18770  injsubmefmnd  18771  smndex1n0mnd  18786  islinds2  21720  pf1ind  22240  ausgrusgrb  29114  upgrres1lem1  29258  cusgrexilem1  29388  sizusglecusg  29413  pliguhgr  30434  bj-evalid  37070  bj-diagval  37168  poimirlem15  37635  xrnidresex  38399  dib0  41163  dicn0  41191  cdlemn11a  41206  dihord6apre  41255  dihatlat  41333  dihpN  41335  eldioph2lem1  42753  eldioph2lem2  42754  dfrtrcl5  43622  dfrcl2  43667  relexpiidm  43697  ushggricedg  47931  uspgrsprfo  48152  rngcidALTV  48278  ringcidALTV  48312  resipos  48979  cofidvala  49121  cofidval  49124  opf2fval  49410  fucoppc  49415  idfudiag1bas  49529  idfudiag1  49530