Theorem elfi

Description: Specific properties of an element of ( fiB ) . (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 24-Nov-2013)

	Ref	Expression
Assertion	elfi	|- ( ( A e. V /\ B e. W ) -> ( A e. ( fi ` B ) <-> E. x e. ( ~P B i^i Fin ) A = |^| x ) )

Proof

Step	Hyp	Ref	Expression
1		fival	|- ( B e. W -> ( fi ` B ) = { y | E. x e. ( ~P B i^i Fin ) y = |^| x } )
2	1	eleq2d	|- ( B e. W -> ( A e. ( fi ` B ) <-> A e. { y | E. x e. ( ~P B i^i Fin ) y = |^| x } ) )
3		eqeq1	|- ( y = A -> ( y = |^| x <-> A = |^| x ) )
4	3	rexbidv	|- ( y = A -> ( E. x e. ( ~P B i^i Fin ) y = |^| x <-> E. x e. ( ~P B i^i Fin ) A = |^| x ) )
5	4	elabg	|- ( A e. V -> ( A e. { y | E. x e. ( ~P B i^i Fin ) y = |^| x } <-> E. x e. ( ~P B i^i Fin ) A = |^| x ) )
6	2 5	sylan9bbr	|- ( ( A e. V /\ B e. W ) -> ( A e. ( fi ` B ) <-> E. x e. ( ~P B i^i Fin ) A = |^| x ) )