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

Metamath Proof Explorer

Theorem elsnres

Description: Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011)

Ref Expression
Hypothesis elsnres.1 
|- C e. _V
Assertion elsnres 
|- ( A e. ( B |` { C } ) <-> E. y ( A = <. C , y >. /\ <. C , y >. e. B ) )

Proof

Step Hyp Ref Expression
1 elsnres.1 
 |-  C e. _V
2 elres 
 |-  ( A e. ( B |` { C } ) <-> E. x e. { C } E. y ( A = <. x , y >. /\ <. x , y >. e. B ) )
3 rexcom4 
 |-  ( E. x e. { C } E. y ( A = <. x , y >. /\ <. x , y >. e. B ) <-> E. y E. x e. { C } ( A = <. x , y >. /\ <. x , y >. e. B ) )
4 opeq1 
 |-  ( x = C -> <. x , y >. = <. C , y >. )
5 4 eqeq2d 
 |-  ( x = C -> ( A = <. x , y >. <-> A = <. C , y >. ) )
6 4 eleq1d 
 |-  ( x = C -> ( <. x , y >. e. B <-> <. C , y >. e. B ) )
7 5 6 anbi12d 
 |-  ( x = C -> ( ( A = <. x , y >. /\ <. x , y >. e. B ) <-> ( A = <. C , y >. /\ <. C , y >. e. B ) ) )
8 1 7 rexsn 
 |-  ( E. x e. { C } ( A = <. x , y >. /\ <. x , y >. e. B ) <-> ( A = <. C , y >. /\ <. C , y >. e. B ) )
9 8 exbii 
 |-  ( E. y E. x e. { C } ( A = <. x , y >. /\ <. x , y >. e. B ) <-> E. y ( A = <. C , y >. /\ <. C , y >. e. B ) )
10 2 3 9 3bitri 
 |-  ( A e. ( B |` { C } ) <-> E. y ( A = <. C , y >. /\ <. C , y >. e. B ) )