Theorem weso 4875

Description: A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997.)

Assertion

Ref	Expression
weso

Proof of Theorem weso

Step	Hyp	Ref	Expression
1		df-we 4845	. 2
2	1	simprbi 464	1

Syntax hints:  ->wi 4  Orwor 4804  Frwfr 4840  Wewwe 4842

This theorem is referenced by:  wecmpep  4876  wetrep  4877  wereu  4880  wereu2  4881  weniso  6250  wexp  6914  ordunifi  7790  ordtypelem7  7970  ordtypelem8  7971  hartogslem1  7988  wofib  7991  wemapso  7997  oemapso  8122  cantnf  8133  cantnfOLD  8155  ween  8437  cflim2  8664  fin23lem27  8729  zorn2lem1  8897  zorn2lem4  8900  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  canth4  9046  canthwelem  9049  pwfseqlem4  9061  ltsopi  9287  wfrlem10  29352  wzel  29380  wsuccl  29383  wsuclb  29384  welb  30227  wepwso  30988  fnwe2lem3  30998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-we 4845