Metamath Proof Explorer

Theorem elrest

Description: The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion elrest 
|- ( ( J e. V /\ B e. W ) -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) )

Proof

Step Hyp Ref Expression
1 restval 
 |-  ( ( J e. V /\ B e. W ) -> ( J |`t B ) = ran ( x e. J |-> ( x i^i B ) ) )
2 1 eleq2d 
 |-  ( ( J e. V /\ B e. W ) -> ( A e. ( J |`t B ) <-> A e. ran ( x e. J |-> ( x i^i B ) ) ) )
3 eqid 
 |-  ( x e. J |-> ( x i^i B ) ) = ( x e. J |-> ( x i^i B ) )
4 vex 
 |-  x e. _V
5 4 inex1 
 |-  ( x i^i B ) e. _V
6 3 5 elrnmpti 
 |-  ( A e. ran ( x e. J |-> ( x i^i B ) ) <-> E. x e. J A = ( x i^i B ) )
7 2 6 bitrdi 
 |-  ( ( J e. V /\ B e. W ) -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) )