Metamath Proof Explorer


Theorem divcl

Description: Closure law for division. (Contributed by NM, 21-Jul-2001) (Proof shortened by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion divcl ABB0AB

Proof

Step Hyp Ref Expression
1 divval ABB0AB=ιx|Bx=A
2 receu ABB0∃!xBx=A
3 riotacl ∃!xBx=Aιx|Bx=A
4 2 3 syl ABB0ιx|Bx=A
5 1 4 eqeltrd ABB0AB