Axiom ax-refl 42

Description: Reflexivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypothesis

Ref	Expression
ax-refl.1	⊢ A:α

Assertion

Ref	Expression
ax-refl	⊢ ⊤⊧(( = A)A)

Detailed syntax breakdown of Axiom ax-refl

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		ke 7	. . . 4 term =
3		ta	. . . 4 term A
4	2, 3	kc 5	. . 3 term ( = A)
5	4, 3	kc 5	. 2 term (( = A)A)
6	1, 5	wffMMJ2 11	1 wff ⊤⊧(( = A)A)

This axiom is referenced by:  wtru  43  eqcomx  52  eqid  83