Theorem eldm1cossres

Description: Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018)

	Ref	Expression
Assertion	eldm1cossres	|- ( B e. V -> ( B e. dom ,~ ( R |` A ) <-> E. u e. A u R B ) )

Proof

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