Definition df-we 5075

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6981. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
df-we	|- ( R We A <-> ( R Fr A /\ R Or A ) )

Detailed syntax breakdown of Definition df-we

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wwe 5072	. 2 wff R We A
4	1, 2	wfr 5070	. . 3 wff R Fr A
5	1, 2	wor 5034	. . 3 wff R Or A
6	4, 5	wa 384	. 2 wff ( R Fr A /\ R Or A )
7	3, 6	wb 196	1 wff ( R We A <-> ( R Fr A /\ R Or A ) )

This definition is referenced by:  nfwe  5090  wess  5101  weeq1  5102  weeq2  5103  wefr  5104  weso  5105  we0  5109  weinxp  5186  wesn  5190  isowe  6599  isowe2  6600  dfwe2  6981  wexp  7291  wofi  8209  dford5reg  31687  fin2so  33396