Given a ∈ ℝ
	If a = 0
		If a ≥ 0
			a = a
		a ≥ 0 ⇒ a = a
		If a ≤ 0
			a = 0 = -0 = -a
			a = -a
		a ≤ 0 ⇒ a = -a
		a ≥ 0 ⇒ a = a ∧ a ≤ 0 ⇒ a = -a
		∃y ∈ ℝ (a ≥ 0 ⇒ y = a ∧ a ≤ 0 ⇒ y = -a)
	If a > 0
		If a ≥ 0
			a = a
		a ≥ 0 ⇒ a = a
		If a ≤ 0
			a > 0
			⊥
			a = -a
		a ≤ 0 ⇒ a = -a
		a ≥ 0 ⇒ a = a ∧ a ≤ 0 ⇒ a = -a
		∃y ∈ ℝ (a ≥ 0 ⇒ y = a ∧ a ≤ 0 ⇒ y = -a)
	If a < 0
		If a ≥ 0
			a < 0
			a ≥ 0
			⊥
			-a = a
		a ≥ 0 ⇒ e = a
		If a ≤ 0
			-a = -a
		a ≥ 0 ⇒ -a = -a
		a ≥ 0 ⇒ -a = a ∧ a ≤ 0 ⇒ -a = -a

@user21820 Is this correct?

@Prithubiswas Almost. You need more brackets on some lines because "∧" has higher precedence than "⇒".

Oh ok. Brackets are needed.

Lol the worst is "a ≥ 0 ⇒ z = a ∧ a ≤ 0 ⇒ z = -a ⇒ z = y" where it is wrong no matter which precedence order you use haha.. =P

Yeah its a mess.

But yea other than that, it's precisely how we get the absolute function on ℝ without any set theory. I would even shorten the "Let abs ∈ obj such that abs = (ℝ x ↦ abs0(x))." to just "Let abs = ( ℝ x ↦ abs0(x) ).".

Argh... I just noticed that I forgot to say T∈set in the function-notation rule.

Oh I see. I didn't need it in the presence of Replacement.

@Prithubiswas: Okay for now you can ignore the last two comments above. All you need to know is that if you can prove any statement of the form S∈set ∧ ∀x∈S ∃!y∈T ( Q(x,y) ) then you can get the corresponding function from S to T in just a few steps via definitorial expansion followed by the function-notation rule.

(You can ignore this comment.) Usually, we also have T∈set, in which case this rule is supported by Set Theory without Replacement (which suffices for all ordinary mathematics). In higher set theory (the study of ZFC itself), we may not have T∈set, but the rule is still supported by Set Theory (with Replacement).

@user21820 Can we prove that ∀x ∈ ℝ ∃!y ∈ ℝ (x ≥ 0 ⇒ y = x)?

@Prithubiswas What if x < 0?

I ommited it on purpose. Just experimenting.

Sorry, my first reaction was correct. What is the truth-value of ∃!y ∈ ℝ (x ≥ 0 ⇒ y = x) when x < 0?

Got to go. Hope you get what this truth-value tells you about whether you can prove ∀x ∈ ℝ ∃!y ∈ ℝ (x ≥ 0 ⇒ y = x). See you!

@user21820 Sure. See you later!

@user21820 I will be away for 2 months due to exams. Hope you don't mind.

@Prithubiswas Sure. All the best for your exams. Take care and see you again next time!