Theorem wunsets

Description: Closure of structure replacement in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	wunsets.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wunsets.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
	wunsets.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	wunsets	⊢ ( 𝜑 → ( 𝑆 sSet 𝐴 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wunsets.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wunsets.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
3		wunsets.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		setsvalg	⊢ ( ( 𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
5	2 3 4	syl2anc	⊢ ( 𝜑 → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
6	1 2	wunres	⊢ ( 𝜑 → ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ 𝑈 )
7	1 3	wunsn	⊢ ( 𝜑 → { 𝐴 } ∈ 𝑈 )
8	1 6 7	wunun	⊢ ( 𝜑 → ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ 𝑈 )
9	5 8	eqeltrd	⊢ ( 𝜑 → ( 𝑆 sSet 𝐴 ) ∈ 𝑈 )