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

Metamath Proof Explorer

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 ⟨ 𝐴 , 𝐶 ⟩ ) )