Theorem eldmres2

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020)

	Ref	Expression
Assertion	eldmres2	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ E. y y e. [ B ] R ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldmres	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ E. y B R y ) ) )
2		eldmg	|- ( B e. V -> ( B e. dom R <-> E. y B R y ) )
3		eldm4	|- ( B e. V -> ( B e. dom R <-> E. y y e. [ B ] R ) )
4	2 3	bitr3d	|- ( B e. V -> ( E. y B R y <-> E. y y e. [ B ] R ) )
5	4	anbi2d	|- ( B e. V -> ( ( B e. A /\ E. y B R y ) <-> ( B e. A /\ E. y y e. [ B ] R ) ) )
6	1 5	bitrd	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ E. y y e. [ B ] R ) ) )