Theorem resiexd 7164

Description: The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.)

Hypothesis

Ref	Expression
resiexd.b	⊢ (𝜑 → 𝐵 ∈ 𝑉)

Assertion

Ref	Expression
resiexd	⊢ (𝜑 → ( I ↾ 𝐵) ∈ V)

Proof of Theorem resiexd

Step	Hyp	Ref	Expression
1		funi 6525	. 2 ⊢ Fun I
2		resiexd.b	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
3		resfunexg 7163	. 2 ⊢ ((Fun I ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐵) ∈ V)
4	1, 2, 3	sylancr 588	1 ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   I cid 5519   ↾ cres 5627  Fun wfun 6487

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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pr 5378

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-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501

This theorem is referenced by:  setcid  18014  estrcid  18061  funcestrcsetclem5  18071  funcsetcestrclem5  18086  funcrngcsetc  20577  funcrngcsetcALT  20578  funcringcsetc  20611  cusgrsize  29511  fzo0pmtrlast  33155  tocycfv  33172  tocycf  33180  lindspropd  33445  rclexi  43892  cnvrcl0  43902  dfrtrcl5  43906  relexp01min  43990  fundcmpsurbijinjpreimafv  47689  fundcmpsurinjALT  47694  ushggricedg  48209  stgrvtx  48236  stgriedg  48237  grlicref  48294  gpgvtx  48325  gpgiedg  48326  uspgrsprfo  48430  rhmsubcALTVlem3  48565  funcringcsetcALTV2lem4  48575  funcringcsetcALTV2lem5  48576  funcringcsetclem4ALTV  48598  funcringcsetclem5ALTV  48599  itcoval0  48944  itcoval1  48945