Theorem resiexg 7866

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903   I cid 5528   × cxp 5632   ↾ cres 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-res 5646

This theorem is referenced by:  ordiso  9435  wdomref  9491  dfac9  10061  relexp0g  14959  relexpsucnnr  14962  ndxarg  17137  idfu2nd  17815  idfu1st  17817  idfucl  17819  funcestrcsetclem4  18080  equivestrcsetc  18089  funcsetcestrclem4  18095  sursubmefmnd  18835  injsubmefmnd  18836  smndex1n0mnd  18854  islinds2  21785  pf1ind  22316  ausgrusgrb  29256  upgrres1lem1  29400  cusgrexilem1  29530  sizusglecusg  29555  pliguhgr  30580  bj-evalid  37356  bj-diagval  37456  poimirlem15  37915  xrnidresex  38710  dib0  41569  dicn0  41597  cdlemn11a  41612  dihord6apre  41661  dihatlat  41739  dihpN  41741  eldioph2lem1  43146  eldioph2lem2  43147  dfrtrcl5  44014  dfrcl2  44059  relexpiidm  44089  ushggricedg  48316  uspgrsprfo  48537  rngcidALTV  48663  ringcidALTV  48697  resipos  49363  cofidvala  49504  cofidval  49507  opf2fval  49793  fucoppc  49798  idfudiag1bas  49912  idfudiag1  49913