Definition df-true-D2.4 155

Description: Definition of True, '⊤'.

Assertion

Ref	Expression
df-true-D2.4	⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))

Detailed syntax breakdown of Definition df-true-D2.4

Step	Hyp	Ref	Expression
1		wff-true 153	. 2 wff ⊤
2		objvar-x	. . . . . 6 objvar 𝑥
3	2	term-obj 1	. . . . 5 term 𝑥
4	3, 3	wff-equals 6	. . . 4 wff 𝑥 = 𝑥
5	4, 2	wff-forall 8	. . 3 wff ∀𝑥 𝑥 = 𝑥
6	5, 5	wff-imp 10	. 2 wff (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
7	1, 6	wff-bi 104	1 wff (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))

This definition is referenced by:  true-P2.14  156