Theorem elrnres

Description: Element of the range of a restriction. (Contributed by Peter Mazsa, 26-Dec-2018)

	Ref	Expression
Assertion	elrnres	|- ( B e. V -> ( B e. ran ( R |` A ) <-> E. x e. A x R B ) )

Proof

Step	Hyp	Ref	Expression
1		elrng	|- ( B e. V -> ( B e. ran ( R |` A ) <-> E. x x ( R |` A ) B ) )
2		brres	|- ( B e. V -> ( x ( R |` A ) B <-> ( x e. A /\ x R B ) ) )
3	2	exbidv	|- ( B e. V -> ( E. x x ( R |` A ) B <-> E. x ( x e. A /\ x R B ) ) )
4	1 3	bitrd	|- ( B e. V -> ( B e. ran ( R |` A ) <-> E. x ( x e. A /\ x R B ) ) )
5		df-rex	|- ( E. x e. A x R B <-> E. x ( x e. A /\ x R B ) )
6	4 5	bitr4di	|- ( B e. V -> ( B e. ran ( R |` A ) <-> E. x e. A x R B ) )