Theorem setsidel

Description: The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Hypotheses	setsidel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	setsidel.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	setsidel.r	⊢ 𝑅 = ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ )
Assertion	setsidel	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		setsidel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		setsidel.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		setsidel.r	⊢ 𝑅 = ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ )
4		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5	4	snid	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ }
6		elun2	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
7	5 6	mp1i	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
8		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
10	3 9	syl5eq	⊢ ( 𝜑 → 𝑅 = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
11	7 10	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )