Metamath Proof Explorer

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 \leftrightarrow (Tr A \land E Or A)$

Proof

Step	Hyp	Ref	Expression
1		df-ord	$⊢ Ord A \leftrightarrow (Tr A \land E We A)$
2		zfregfr	$⊢ E Fr A$
3		df-we	$⊢ E We A \leftrightarrow (E Fr A \land E Or A)$
4	2 3	mpbiran	$⊢ E We A \leftrightarrow E Or A$
5	4	anbi2i	$⊢ (Tr A \land E We A) \leftrightarrow (Tr A \land E Or A)$
6	1 5	bitri	$⊢ Ord A \leftrightarrow (Tr A \land E Or A)$