MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wefr Unicode version

Theorem wefr 4532
Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
Assertion
Ref Expression
wefr  |-  ( R  We  A  ->  R  Fr  A )

Proof of Theorem wefr
StepHypRef Expression
1 df-we 4503 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
21simplbi 447 1  |-  ( R  We  A  ->  R  Fr  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Or wor 4462    Fr wfr 4498    We wwe 4500
This theorem is referenced by:  wefrc  4536  wereu  4538  wereu2  4539  ordfr  4556  wexp  6419  wofib  7470  wemapso  7476  wemapso2  7477  cflim2  8099  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  wfrlem14  25483  welb  26328  fnwe2lem2  27016  onfrALTlem3  28341  onfrALTlem3VD  28708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-we 4503
  Copyright terms: Public domain W3C validator