Theorem intimasn

Description: Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimasn	|- ( B e. V -> ( |^| A " { B } ) = |^| { x | E. a e. A x = ( a " { B } ) } )

Proof

Step	Hyp	Ref	Expression
1		ax-5	|- ( B e. V -> A. y B e. V )
2		r19.12sn	|- ( B e. V -> ( E. b e. { B } A. a e. A <. b , y >. e. a <-> A. a e. A E. b e. { B } <. b , y >. e. a ) )
3	2	biimprd	|- ( B e. V -> ( A. a e. A E. b e. { B } <. b , y >. e. a -> E. b e. { B } A. a e. A <. b , y >. e. a ) )
4	3	alimi	|- ( A. y B e. V -> A. y ( A. a e. A E. b e. { B } <. b , y >. e. a -> E. b e. { B } A. a e. A <. b , y >. e. a ) )
5		intimag	|- ( A. y ( A. a e. A E. b e. { B } <. b , y >. e. a -> E. b e. { B } A. a e. A <. b , y >. e. a ) -> ( |^| A " { B } ) = |^| { x | E. a e. A x = ( a " { B } ) } )
6	1 4 5	3syl	|- ( B e. V -> ( |^| A " { B } ) = |^| { x | E. a e. A x = ( a " { B } ) } )