This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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