Theorem bj-restsnss

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

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

Proof

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