Theorem dvdsr2

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

	Ref	Expression
Hypotheses	dvdsr.1	|- B = ( Base ` R )
	dvdsr.2	|- .|| = ( ||r ` R )
	dvdsr.3	|- .x. = ( .r ` R )
Assertion	dvdsr2	|- ( X e. B -> ( X .|| Y <-> E. z e. B ( z .x. X ) = Y ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	|- B = ( Base ` R )
2		dvdsr.2	|- .|| = ( ||r ` R )
3		dvdsr.3	|- .x. = ( .r ` R )
4	1 2 3	dvdsr	|- ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) )
5	4	baib	|- ( X e. B -> ( X .|| Y <-> E. z e. B ( z .x. X ) = Y ) )