Theorem eldmcnv

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

	Ref	Expression
Assertion	eldmcnv	$$⊢A\in V\to \left(A\in \mathrm{dom}{R}^{-1}\leftrightarrow \exists uuRA\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldmg	$$⊢A\in V\to \left(A\in \mathrm{dom}{R}^{-1}\leftrightarrow \exists uA{R}^{-1}u\right)$$
2		brcnvg	$$⊢\left(A\in V\wedge u\in \mathrm{V}\right)\to \left(A{R}^{-1}u\leftrightarrow uRA\right)$$
3	2	elvd	$$⊢A\in V\to \left(A{R}^{-1}u\leftrightarrow uRA\right)$$
4	3	exbidv	$$⊢A\in V\to \left(\exists uA{R}^{-1}u\leftrightarrow \exists uuRA\right)$$
5	1 4	bitrd	$$⊢A\in V\to \left(A\in \mathrm{dom}{R}^{-1}\leftrightarrow \exists uuRA\right)$$