Theorem eldmcoss2

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

	Ref	Expression
Assertion	eldmcoss2	|- ( A e. V -> ( A e. dom ,~ R <-> A ,~ R A ) )

Proof

Step	Hyp	Ref	Expression
1		eldmcoss	|- ( A e. V -> ( A e. dom ,~ R <-> E. u u R A ) )
2		brcoss	|- ( ( A e. V /\ A e. V ) -> ( A ,~ R A <-> E. u ( u R A /\ u R A ) ) )
3	2	anidms	|- ( A e. V -> ( A ,~ R A <-> E. u ( u R A /\ u R A ) ) )
4		pm4.24	|- ( u R A <-> ( u R A /\ u R A ) )
5	4	exbii	|- ( E. u u R A <-> E. u ( u R A /\ u R A ) )
6	3 5	bitr4di	|- ( A e. V -> ( A ,~ R A <-> E. u u R A ) )
7	1 6	bitr4d	|- ( A e. V -> ( A e. dom ,~ R <-> A ,~ R A ) )