This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )