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	$$⊢\left(\mathrm{Tr}A\wedge B\in A\right)\to B\subset A$$

Proof

Step	Hyp	Ref	Expression
1		zfregfr	$$⊢\mathrm{E}\mathrm{Fr}A$$
2		tz7.2	$$⊢\left(\mathrm{Tr}A\wedge \mathrm{E}\mathrm{Fr}A\wedge B\in A\right)\to \left(B\subseteq A\wedge B\ne A\right)$$
3	1 2	mp3an2	$$⊢\left(\mathrm{Tr}A\wedge B\in A\right)\to \left(B\subseteq A\wedge B\ne A\right)$$
4		df-pss	$$⊢B\subset A\leftrightarrow \left(B\subseteq A\wedge B\ne A\right)$$
5	3 4	sylibr	$$⊢\left(\mathrm{Tr}A\wedge B\in A\right)\to B\subset A$$