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