Metamath Proof Explorer

Theorem elres

Description: Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011) (Proof shortened by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elres 
|- ( A e. ( B |` C ) <-> E. x e. C E. y ( A = <. x , y >. /\ <. x , y >. e. B ) )

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( B |` C ) = ( B i^i ( C X. _V ) )
2 1 eleq2i 
 |-  ( A e. ( B |` C ) <-> A e. ( B i^i ( C X. _V ) ) )
3 elinxp 
 |-  ( A e. ( B i^i ( C X. _V ) ) <-> E. x e. C E. y e. _V ( A = <. x , y >. /\ <. x , y >. e. B ) )
4 rexv 
 |-  ( E. y e. _V ( A = <. x , y >. /\ <. x , y >. e. B ) <-> E. y ( A = <. x , y >. /\ <. x , y >. e. B ) )
5 4 rexbii 
 |-  ( E. x e. C E. y e. _V ( A = <. x , y >. /\ <. x , y >. e. B ) <-> E. x e. C E. y ( A = <. x , y >. /\ <. x , y >. e. B ) )
6 2 3 5 3bitri 
 |-  ( A e. ( B |` C ) <-> E. x e. C E. y ( A = <. x , y >. /\ <. x , y >. e. B ) )