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

Metamath Proof Explorer

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 biimtrid 
 |-  ( ( 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 imbitrdi 
 |-  ( ( 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 ) )