Theorem eldm4

Description: Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018)

	Ref	Expression
Assertion	eldm4	$$⊢A\in V\to \left(A\in \mathrm{dom}R\leftrightarrow \exists yy\in \left[A\right]R\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldmg	$$⊢A\in V\to \left(A\in \mathrm{dom}R\leftrightarrow \exists yARy\right)$$
2		elecALTV	$$⊢\left(A\in V\wedge y\in \mathrm{V}\right)\to \left(y\in \left[A\right]R\leftrightarrow ARy\right)$$
3	2	elvd	$$⊢A\in V\to \left(y\in \left[A\right]R\leftrightarrow ARy\right)$$
4	3	exbidv	$$⊢A\in V\to \left(\exists yy\in \left[A\right]R\leftrightarrow \exists yARy\right)$$
5	1 4	bitr4d	$$⊢A\in V\to \left(A\in \mathrm{dom}R\leftrightarrow \exists yy\in \left[A\right]R\right)$$