Metamath Proof Explorer


Theorem wunsets

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

Ref Expression
Hypotheses wunsets.1 φ U WUni
wunsets.2 φ S U
wunsets.3 φ A U
Assertion wunsets φ S sSet A U

Proof

Step Hyp Ref Expression
1 wunsets.1 φ U WUni
2 wunsets.2 φ S U
3 wunsets.3 φ A U
4 setsvalg S U A U S sSet A = S V dom A A
5 2 3 4 syl2anc φ S sSet A = S V dom A A
6 1 2 wunres φ S V dom A U
7 1 3 wunsn φ A U
8 1 6 7 wunun φ S V dom A A U
9 5 8 eqeltrd φ S sSet A U