ordeq

Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993)

		Ref	Expression
	Assertion	ordeq	$⊢ A = B \to (Ord A \leftrightarrow Ord B)$

Step	Hyp	Ref	Expression
1		treq	$⊢ A = B \to (Tr A \leftrightarrow Tr B)$
2		weeq2	$⊢ A = B \to (E We A \leftrightarrow E We B)$
3	1 2	anbi12d	$⊢ A = B \to ((Tr A \land E We A) \leftrightarrow (Tr B \land E We B))$
4		df-ord	$⊢ Ord A \leftrightarrow (Tr A \land E We A)$
5		df-ord	$⊢ Ord B \leftrightarrow (Tr B \land E We B)$
6	3 4 5	3bitr4g	$⊢ A = B \to (Ord A \leftrightarrow Ord B)$

Metamath Proof Explorer