Theorem bj-restsn

Description: An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 and bj-restsnid . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsn	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } )

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 𝑌 } ∈ V
2		elrest	⊢ ( ( { 𝑌 } ∈ V ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝑌 } ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ { 𝑌 } 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑥 ∈ ( { 𝑌 } ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ { 𝑌 } 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
4		velsn	⊢ ( 𝑥 ∈ { ( 𝑦 ∩ 𝐴 ) } ↔ 𝑥 = ( 𝑦 ∩ 𝐴 ) )
5		ineq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∩ 𝐴 ) = ( 𝑌 ∩ 𝐴 ) )
6	5	sneqd	⊢ ( 𝑦 = 𝑌 → { ( 𝑦 ∩ 𝐴 ) } = { ( 𝑌 ∩ 𝐴 ) } )
7	6	eleq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑥 ∈ { ( 𝑦 ∩ 𝐴 ) } ↔ 𝑥 ∈ { ( 𝑌 ∩ 𝐴 ) } ) )
8	4 7	bitr3id	⊢ ( 𝑦 = 𝑌 → ( 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ 𝑥 ∈ { ( 𝑌 ∩ 𝐴 ) } ) )
9	8	rexsng	⊢ ( 𝑌 ∈ 𝑉 → ( ∃ 𝑦 ∈ { 𝑌 } 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ 𝑥 ∈ { ( 𝑌 ∩ 𝐴 ) } ) )
10	3 9	sylan9bbr	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝑌 } ↾t 𝐴 ) ↔ 𝑥 ∈ { ( 𝑌 ∩ 𝐴 ) } ) )
11	10	eqrdv	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } )