metamath/valid/mathd-algebra-104.mm

$(
  @{
    mathd-algebra-104.0 @e |- ( ph -> X e. RR ) $@
    mathd-algebra-104.1 @e |- ( ph -> ( ; ; 1 2 5 / 8 ) = ( X / ; 1 2 ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-104 @p |- ( ph -> X = ( ; ; 3 7 5 / 2 ) ) @=
      ? @.
  @}
$)