Theorem bj-elres

Description: Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011) (Proof shortened by Peter Mazsa, 9-Sep-2022) Use the x B y idiom. (Revised by BJ, 16-Oct-2026)

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

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		bj-elinxp	|- ( A e. ( B i^i ( C X. _V ) ) <-> E. x e. C E. y e. _V ( A = <. x , y >. /\ x B y ) )
4		rexv	|- ( E. y e. _V ( A = <. x , y >. /\ x B y ) <-> E. y ( A = <. x , y >. /\ x B y ) )
5	4	rexbii	|- ( E. x e. C E. y e. _V ( A = <. x , y >. /\ x B y ) <-> E. x e. C E. y ( A = <. x , y >. /\ x B y ) )
6	2 3 5	3bitri	|- ( A e. ( B |` C ) <-> E. x e. C E. y ( A = <. x , y >. /\ x B y ) )