Theorem dvdsr2

Description: Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
	dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	dvdsr.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	dvdsr2	$$⊢X\in B\to \left(X\underset{\dot{}}{\parallel }Y\leftrightarrow \exists z\in Bz\underset{\dot{}}{·}X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		dvdsr.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4	1 2 3	dvdsr	$$⊢X\underset{\dot{}}{\parallel }Y\leftrightarrow \left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\right)$$
5	4	baib	$$⊢X\in B\to \left(X\underset{\dot{}}{\parallel }Y\leftrightarrow \exists z\in Bz\underset{\dot{}}{·}X=Y\right)$$