Theorem ssdmral

Description: Subclass of a domain. (Contributed by Peter Mazsa, 15-Sep-2018)

	Ref	Expression
Assertion	ssdmral	$$⊢A\subseteq \mathrm{dom}R\leftrightarrow \forall x\in A\exists yxRy$$

Proof

Step	Hyp	Ref	Expression
1		dfss3	$$⊢A\subseteq \mathrm{dom}R\leftrightarrow \forall x\in Ax\in \mathrm{dom}R$$
2		eldmg	$$⊢x\in \mathrm{V}\to \left(x\in \mathrm{dom}R\leftrightarrow \exists yxRy\right)$$
3	2	elv	$$⊢x\in \mathrm{dom}R\leftrightarrow \exists yxRy$$
4	3	ralbii	$$⊢\forall x\in Ax\in \mathrm{dom}R\leftrightarrow \forall x\in A\exists yxRy$$
5	1 4	bitri	$$⊢A\subseteq \mathrm{dom}R\leftrightarrow \forall x\in A\exists yxRy$$