Theorem setsv

Description: The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Assertion	setsv	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
2		resexg	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∈ V )
3		snex	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V
4	3	a1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V )
5		unexg	⊢ ( ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∈ V ∧ { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V ) → ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ∈ V )
6	2 4 5	syl2an2r	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ∈ V )
7	1 6	eqeltrd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V )