Theorem ressunif

Description: UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017)

	Ref	Expression
Hypotheses	ressunif.1	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
	ressunif.2	⊢ 𝑈 = ( UnifSet ‘ 𝐺 )
Assertion	ressunif	⊢ ( 𝐴 ∈ 𝑉 → 𝑈 = ( UnifSet ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		ressunif.1	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2		ressunif.2	⊢ 𝑈 = ( UnifSet ‘ 𝐺 )
3		df-unif	⊢ UnifSet = Slot ; 1 3
4		1nn0	⊢ 1 ∈ ℕ0
5		3nn	⊢ 3 ∈ ℕ
6	4 5	decnncl	⊢ ; 1 3 ∈ ℕ
7		1nn	⊢ 1 ∈ ℕ
8		3nn0	⊢ 3 ∈ ℕ0
9		1lt10	⊢ 1 < ; 1 0
10	7 8 4 9	declti	⊢ 1 < ; 1 3
11	1 2 3 6 10	resslem	⊢ ( 𝐴 ∈ 𝑉 → 𝑈 = ( UnifSet ‘ 𝐻 ) )