Theorem eldmcnv

Description: Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018)

	Ref	Expression
Assertion	eldmcnv	|- ( A e. V -> ( A e. dom `' R <-> E. u u R A ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	|- ( A e. V -> ( A e. dom `' R <-> E. u A `' R u ) )
2		brcnvg	|- ( ( A e. V /\ u e. _V ) -> ( A `' R u <-> u R A ) )
3	2	elvd	|- ( A e. V -> ( A `' R u <-> u R A ) )
4	3	exbidv	|- ( A e. V -> ( E. u A `' R u <-> E. u u R A ) )
5	1 4	bitrd	|- ( A e. V -> ( A e. dom `' R <-> E. u u R A ) )