Theorem resiexg 7891

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917   I cid 5535   × cxp 5639   ↾ cres 5643

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-res 5653

This theorem is referenced by:  ordiso  9476  wdomref  9532  dfac9  10097  relexp0g  14995  relexpsucnnr  14998  ndxarg  17173  idfu2nd  17846  idfu1st  17848  idfucl  17850  funcestrcsetclem4  18111  equivestrcsetc  18120  funcsetcestrclem4  18126  sursubmefmnd  18830  injsubmefmnd  18831  smndex1n0mnd  18846  islinds2  21729  pf1ind  22249  ausgrusgrb  29099  upgrres1lem1  29243  cusgrexilem1  29373  sizusglecusg  29398  pliguhgr  30422  bj-evalid  37071  bj-diagval  37169  poimirlem15  37636  xrnidresex  38400  dib0  41165  dicn0  41193  cdlemn11a  41208  dihord6apre  41257  dihatlat  41335  dihpN  41337  eldioph2lem1  42755  eldioph2lem2  42756  dfrtrcl5  43625  dfrcl2  43670  relexpiidm  43700  ushggricedg  47931  uspgrsprfo  48140  rngcidALTV  48266  ringcidALTV  48300  resipos  48967  cofidvala  49109  cofidval  49112  opf2fval  49398  fucoppc  49403  idfudiag1bas  49517  idfudiag1  49518