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	⊢ −_ℝ = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ℩ 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) )

Metamath Proof Explorer

Definition df-resub

Detailed syntax breakdown