Metamath Proof Explorer

Theorem setsvalg

Description: Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion setsvalg ⊢ S ∈ V ∧ A ∈ W → S sSet A = S ↾ V ∖ dom ⁡ A ∪ A

Proof

Step Hyp Ref Expression
1 elex ⊢ S ∈ V → S ∈ V
2 elex ⊢ A ∈ W → A ∈ V
3 resexg ⊢ S ∈ V → S ↾ V ∖ dom ⁡ A ∈ V
4 3 adantr ⊢ S ∈ V ∧ A ∈ V → S ↾ V ∖ dom ⁡ A ∈ V
5 snex ⊢ A ∈ V
6 unexg ⊢ S ↾ V ∖ dom ⁡ A ∈ V ∧ A ∈ V → S ↾ V ∖ dom ⁡ A ∪ A ∈ V
7 4 5 6 sylancl ⊢ S ∈ V ∧ A ∈ V → S ↾ V ∖ dom ⁡ A ∪ A ∈ V
8 simpl ⊢ s = S ∧ e = A → s = S
9 simpr ⊢ s = S ∧ e = A → e = A
10 9 sneqd ⊢ s = S ∧ e = A → e = A
11 10 dmeqd ⊢ s = S ∧ e = A → dom ⁡ e = dom ⁡ A
12 11 difeq2d ⊢ s = S ∧ e = A → V ∖ dom ⁡ e = V ∖ dom ⁡ A
13 8 12 reseq12d ⊢ s = S ∧ e = A → s ↾ V ∖ dom ⁡ e = S ↾ V ∖ dom ⁡ A
14 13 10 uneq12d ⊢ s = S ∧ e = A → s ↾ V ∖ dom ⁡ e ∪ e = S ↾ V ∖ dom ⁡ A ∪ A
15 df-sets ⊢ sSet = s ∈ V , e ∈ V ⟼ s ↾ V ∖ dom ⁡ e ∪ e
16 14 15 ovmpoga ⊢ S ∈ V ∧ A ∈ V ∧ S ↾ V ∖ dom ⁡ A ∪ A ∈ V → S sSet A = S ↾ V ∖ dom ⁡ A ∪ A
17 7 16 mpd3an3 ⊢ S ∈ V ∧ A ∈ V → S sSet A = S ↾ V ∖ dom ⁡ A ∪ A
18 1 2 17 syl2an ⊢ S ∈ V ∧ A ∈ W → S sSet A = S ↾ V ∖ dom ⁡ A ∪ A