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 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊊ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		zfregfr	⊢ E Fr 𝐴
2		tz7.2	⊢ ( ( Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
3	1 2	mp3an2	⊢ ( ( Tr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
4		df-pss	⊢ ( 𝐵 ⊊ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
5	3 4	sylibr	⊢ ( ( Tr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊊ 𝐴 )