Theorem dford5reg

Description: Given ax-reg , an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011)

	Ref	Expression
Assertion	dford5reg	|- ( Ord A <-> ( Tr A /\ _E Or A ) )

Proof

Step	Hyp	Ref	Expression
1		df-ord	|- ( Ord A <-> ( Tr A /\ _E We A ) )
2		zfregfr	|- _E Fr A
3		df-we	|- ( _E We A <-> ( _E Fr A /\ _E Or A ) )
4	2 3	mpbiran	|- ( _E We A <-> _E Or A )
5	4	anbi2i	|- ( ( Tr A /\ _E We A ) <-> ( Tr A /\ _E Or A ) )
6	1 5	bitri	|- ( Ord A <-> ( Tr A /\ _E Or A ) )