Theorem trin

Description: The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994)

	Ref	Expression
Assertion	trin	|- ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2		trss	|- ( Tr A -> ( x e. A -> x C_ A ) )
3		trss	|- ( Tr B -> ( x e. B -> x C_ B ) )
4	2 3	im2anan9	|- ( ( Tr A /\ Tr B ) -> ( ( x e. A /\ x e. B ) -> ( x C_ A /\ x C_ B ) ) )
5	1 4	syl5bi	|- ( ( Tr A /\ Tr B ) -> ( x e. ( A i^i B ) -> ( x C_ A /\ x C_ B ) ) )
6		ssin	|- ( ( x C_ A /\ x C_ B ) <-> x C_ ( A i^i B ) )
7	5 6	syl6ib	|- ( ( Tr A /\ Tr B ) -> ( x e. ( A i^i B ) -> x C_ ( A i^i B ) ) )
8	7	ralrimiv	|- ( ( Tr A /\ Tr B ) -> A. x e. ( A i^i B ) x C_ ( A i^i B ) )
9		dftr3	|- ( Tr ( A i^i B ) <-> A. x e. ( A i^i B ) x C_ ( A i^i B ) )
10	8 9	sylibr	|- ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )