Theorem wunsets

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

	Ref	Expression
Hypotheses	wunsets.1	|- ( ph -> U e. WUni )
	wunsets.2	|- ( ph -> S e. U )
	wunsets.3	|- ( ph -> A e. U )
Assertion	wunsets	|- ( ph -> ( S sSet A ) e. U )

Proof

Step	Hyp	Ref	Expression
1		wunsets.1	|- ( ph -> U e. WUni )
2		wunsets.2	|- ( ph -> S e. U )
3		wunsets.3	|- ( ph -> A e. U )
4		setsvalg	|- ( ( S e. U /\ A e. U ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
5	2 3 4	syl2anc	|- ( ph -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
6	1 2	wunres	|- ( ph -> ( S |` ( _V \ dom { A } ) ) e. U )
7	1 3	wunsn	|- ( ph -> { A } e. U )
8	1 6 7	wunun	|- ( ph -> ( ( S |` ( _V \ dom { A } ) ) u. { A } ) e. U )
9	5 8	eqeltrd	|- ( ph -> ( S sSet A ) e. U )