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  10068  relexp0g  14965  relexpsucnnr  14968  ndxarg  17143  idfu2nd  17820  idfu1st  17822  idfucl  17824  funcestrcsetclem4  18085  equivestrcsetc  18094  funcsetcestrclem4  18100  sursubmefmnd  18806  injsubmefmnd  18807  smndex1n0mnd  18822  islinds2  21756  pf1ind  22276  ausgrusgrb  29146  upgrres1lem1  29290  cusgrexilem1  29420  sizusglecusg  29445  pliguhgr  30466  bj-evalid  37058  bj-diagval  37156  poimirlem15  37623  xrnidresex  38387  dib0  41152  dicn0  41180  cdlemn11a  41195  dihord6apre  41244  dihatlat  41322  dihpN  41324  eldioph2lem1  42742  eldioph2lem2  42743  dfrtrcl5  43612  dfrcl2  43657  relexpiidm  43687  ushggricedg  47921  uspgrsprfo  48130  rngcidALTV  48256  ringcidALTV  48290  resipos  48957  cofidvala  49099  cofidval  49102  opf2fval  49388  fucoppc  49393  idfudiag1bas  49507  idfudiag1  49508