This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trsucss

Description: A member of the successor of a transitive class is a subclass of it. Lemma 1.13 of Schloeder p. 2. (Contributed by NM, 4-Oct-2003)

		Ref	Expression
	Assertion	trsucss	$⊢ Tr A \to (B \in suc A \to B \subseteq A)$

Step	Hyp	Ref	Expression
1		elsuci	$⊢ B \in suc A \to (B \in A \lor B = A)$
2		trss	$⊢ Tr A \to (B \in A \to B \subseteq A)$
3		eqimss	$⊢ B = A \to B \subseteq A$
4	3	a1i	$⊢ Tr A \to (B = A \to B \subseteq A)$
5	2 4	jaod	$⊢ Tr A \to ((B \in A \lor B = A) \to B \subseteq A)$
6	1 5	syl5	$⊢ Tr A \to (B \in suc A \to B \subseteq A)$