Theorem setsabs

Description: Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	setsabs	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		setsres	⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )
2	1	adantr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )
3	2	uneq1d	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
4		ovexd	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V )
5		setsval	⊢ ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
6	4 5	sylan	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
7		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
8	3 6 7	3eqtr4d	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) sSet ⟨ 𝐴 , 𝐶 ⟩ ) = ( 𝑆 sSet ⟨ 𝐴 , 𝐶 ⟩ ) )