Metamath Proof Explorer


Definition df-resub

Description: Define subtraction between real numbers. This operator saves a few axioms over df-sub in certain situations. Theorem resubval shows its value, resubadd relates it to addition, and rersubcl proves its closure. It is the restriction of df-sub to the reals: subresre . (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion df-resub = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cresub
1 vx 𝑥
2 cr
3 vy 𝑦
4 vz 𝑧
5 3 cv 𝑦
6 caddc +
7 4 cv 𝑧
8 5 7 6 co ( 𝑦 + 𝑧 )
9 1 cv 𝑥
10 8 9 wceq ( 𝑦 + 𝑧 ) = 𝑥
11 10 4 2 crio ( 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 )
12 1 3 2 2 11 cmpo ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) )
13 0 12 wceq = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) )