Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ transitive x, hypo.
03. 3 ⊢ u ∈ x ∪ {x}, hypo.
04. 3 ⊢ u ∈ x ∨ u ∈ {x}, union_elim 3.
05. 5 ⊢ u ∈ x, hypo.
06. 2, 5 ⊢ u ⊆ x, transitive_elim 2 5.
07. 7 ⊢ u ∈ {x}, hypo.
08. 1, 7 ⊢ u = x, sg_elim 1 7.
09. 1, 7 ⊢ u ⊆ x, incl_from_eq 8.
10. 1, 2, 3 ⊢ u ⊆ x, disj_elim 4 6 9.
11. ⊢ x ⊆ x ∪ {x}, union_incl_left.
12. 1, 2, 3 ⊢ u ⊆ x ∪ {x}, incl_trans 10 11.
13. 1, 2 ⊢ u ∈ x ∪ {x} → u ⊆ x ∪ {x}, subj_intro 12.
14. 1, 2 ⊢ ∀u. u ∈ x ∪ {x} → u ⊆ x ∪ {x}, uq_intro 13.
15. 1, 2 ⊢ transitive (x ∪ {x}), transitive_intro 14.
transitive_closed_succ. ⊢ set x → transitive x →
transitive (x ∪ {x}), subj_intro_ii 15.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.