Theorem eldm1cossres2

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

	Ref	Expression
Assertion	eldm1cossres2	|- ( B e. V -> ( B e. dom ,~ ( R |` A ) <-> E. x e. A B e. [ x ] R ) )

Proof

Step	Hyp	Ref	Expression
1		eldm1cossres	|- ( B e. V -> ( B e. dom ,~ ( R |` A ) <-> E. x e. A x R B ) )
2		elecALTV	|- ( ( x e. _V /\ B e. V ) -> ( B e. [ x ] R <-> x R B ) )
3	2	el2v1	|- ( B e. V -> ( B e. [ x ] R <-> x R B ) )
4	3	rexbidv	|- ( B e. V -> ( E. x e. A B e. [ x ] R <-> E. x e. A x R B ) )
5	1 4	bitr4d	|- ( B e. V -> ( B e. dom ,~ ( R |` A ) <-> E. x e. A B e. [ x ] R ) )