Theorem weeq2

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994)

	Ref	Expression
Assertion	weeq2	|- ( A = B -> ( R We A <-> R We B ) )

Proof

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