Theorem weeq1

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997)

	Ref	Expression
Assertion	weeq1	$$⊢R=S\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		freq1	$$⊢R=S\to \left(R\mathrm{Fr}A\leftrightarrow S\mathrm{Fr}A\right)$$
2		soeq1	$$⊢R=S\to \left(R\mathrm{Or}A\leftrightarrow S\mathrm{Or}A\right)$$
3	1 2	anbi12d	$$⊢R=S\to \left(\left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)\leftrightarrow \left(S\mathrm{Fr}A\wedge S\mathrm{Or}A\right)\right)$$
4		df-we	$$⊢R\mathrm{We}A\leftrightarrow \left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)$$
5		df-we	$$⊢S\mathrm{We}A\leftrightarrow \left(S\mathrm{Fr}A\wedge S\mathrm{Or}A\right)$$
6	3 4 5	3bitr4g	$$⊢R=S\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}A\right)$$