This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-rediv

Description: Define division between real numbers. This operator saves ax-mulcom over df-div in certain situations. (Contributed by SN, 25-Nov-2025)

Ref Expression
Assertion df-rediv Could not format assertion : No typesetting found for |- /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 crediv Could not format /R : No typesetting found for class /R with typecode class
1 vx setvar x
2 cr class ℝ
3 vy setvar y
4 cc0 class 0
5 4 csn class 0
6 2 5 cdif class ℝ ∖ 0
7 vz setvar z
8 3 cv setvar y
9 cmul class ×
10 7 cv setvar z
11 8 10 9 co class y ⁢ z
12 1 cv setvar x
13 11 12 wceq wff y ⁢ z = x
14 13 7 2 crio class ι z ∈ ℝ | y ⁢ z = x
15 1 3 2 6 14 cmpo class x ∈ ℝ , y ∈ ℝ ∖ 0 ⟼ ι z ∈ ℝ | y ⁢ z = x
16 0 15 wceq Could not format /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) ) : No typesetting found for wff /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) ) with typecode wff