Theorem weeq1

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

	Ref	Expression
Assertion	weeq1	|- ( R = S -> ( R We A <-> S We A ) )

Proof

Step	Hyp	Ref	Expression
1		freq1	|- ( R = S -> ( R Fr A <-> S Fr A ) )
2		soeq1	|- ( R = S -> ( R Or A <-> S Or A ) )
3	1 2	anbi12d	|- ( R = S -> ( ( R Fr A /\ R Or A ) <-> ( S Fr A /\ S Or A ) ) )
4		df-we	|- ( R We A <-> ( R Fr A /\ R Or A ) )
5		df-we	|- ( S We A <-> ( S Fr A /\ S Or A ) )
6	3 4 5	3bitr4g	|- ( R = S -> ( R We A <-> S We A ) )