Theorem bj-restsnss2

Description: Special case of bj-restsn . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsnss2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴 ) → ( { 𝑌 } ↾t 𝐴 ) = { 𝑌 } )

Proof

Step	Hyp	Ref	Expression
1		df-ss	⊢ ( 𝑌 ⊆ 𝐴 ↔ ( 𝑌 ∩ 𝐴 ) = 𝑌 )
2		sneq	⊢ ( ( 𝑌 ∩ 𝐴 ) = 𝑌 → { ( 𝑌 ∩ 𝐴 ) } = { 𝑌 } )
3	1 2	sylbi	⊢ ( 𝑌 ⊆ 𝐴 → { ( 𝑌 ∩ 𝐴 ) } = { 𝑌 } )
4		ssexg	⊢ ( ( 𝑌 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝑌 ∈ V )
5	4	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴 ) → 𝑌 ∈ V )
6		bj-restsn	⊢ ( ( 𝑌 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } )
7	6	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ V ) → ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } )
8	5 7	syldan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴 ) → ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } )
9		eqeq2	⊢ ( { ( 𝑌 ∩ 𝐴 ) } = { 𝑌 } → ( ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } ↔ ( { 𝑌 } ↾t 𝐴 ) = { 𝑌 } ) )
10	9	biimpa	⊢ ( ( { ( 𝑌 ∩ 𝐴 ) } = { 𝑌 } ∧ ( { 𝑌 } ↾t 𝐴 ) = { ( 𝑌 ∩ 𝐴 ) } ) → ( { 𝑌 } ↾t 𝐴 ) = { 𝑌 } )
11	3 8 10	syl2an2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴 ) → ( { 𝑌 } ↾t 𝐴 ) = { 𝑌 } )