Metamath Proof Explorer

Theorem trelpss

Description: An element of a transitive set is a proper subset of it. Theorem 7.2 in TakeutiZaring p. 35. Unlike tz7.2 , ax-reg is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011)

Ref Expression
Assertion trelpss 
|- ( ( Tr A /\ B e. A ) -> B C. A )

Proof

Step Hyp Ref Expression
1 zfregfr 
 |-  _E Fr A
2 tz7.2 
 |-  ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) )
3 1 2 mp3an2 
 |-  ( ( Tr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) )
4 df-pss 
 |-  ( B C. A <-> ( B C_ A /\ B =/= A ) )
5 3 4 sylibr 
 |-  ( ( Tr A /\ B e. A ) -> B C. A )