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	|- ( ( Y e. V /\ A e. W ) -> ( { Y } |`t A ) = { ( Y i^i A ) } )

Proof

Step	Hyp	Ref	Expression
1		snex	|- { Y } e. _V
2		elrest	|- ( ( { Y } e. _V /\ A e. W ) -> ( x e. ( { Y } |`t A ) <-> E. y e. { Y } x = ( y i^i A ) ) )
3	1 2	mpan	|- ( A e. W -> ( x e. ( { Y } |`t A ) <-> E. y e. { Y } x = ( y i^i A ) ) )
4		velsn	|- ( x e. { ( y i^i A ) } <-> x = ( y i^i A ) )
5		ineq1	|- ( y = Y -> ( y i^i A ) = ( Y i^i A ) )
6	5	sneqd	|- ( y = Y -> { ( y i^i A ) } = { ( Y i^i A ) } )
7	6	eleq2d	|- ( y = Y -> ( x e. { ( y i^i A ) } <-> x e. { ( Y i^i A ) } ) )
8	4 7	bitr3id	|- ( y = Y -> ( x = ( y i^i A ) <-> x e. { ( Y i^i A ) } ) )
9	8	rexsng	|- ( Y e. V -> ( E. y e. { Y } x = ( y i^i A ) <-> x e. { ( Y i^i A ) } ) )
10	3 9	sylan9bbr	|- ( ( Y e. V /\ A e. W ) -> ( x e. ( { Y } |`t A ) <-> x e. { ( Y i^i A ) } ) )
11	10	eqrdv	|- ( ( Y e. V /\ A e. W ) -> ( { Y } |`t A ) = { ( Y i^i A ) } )