Theorem bj-restsnid

Description: The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn and bj-restsnss . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsnid	|- ( { A } |`t A ) = { A }

Proof

Step	Hyp	Ref	Expression
1		ssid	|- A C_ A
2		bj-restsnss	|- ( ( A e. _V /\ A C_ A ) -> ( { A } |`t A ) = { A } )
3	1 2	mpan2	|- ( A e. _V -> ( { A } |`t A ) = { A } )
4		df-rest	|- |`t = ( x e. _V , y e. _V |-> ran ( z e. x |-> ( z i^i y ) ) )
5	4	reldmmpo	|- Rel dom |`t
6	5	ovprc2	|- ( -. A e. _V -> ( { A } |`t A ) = (/) )
7		snprc	|- ( -. A e. _V <-> { A } = (/) )
8	7	biimpi	|- ( -. A e. _V -> { A } = (/) )
9	6 8	eqtr4d	|- ( -. A e. _V -> ( { A } |`t A ) = { A } )
10	3 9	pm2.61i	|- ( { A } |`t A ) = { A }