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

Theorem wefr 5094
Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
Assertion
Ref Expression
wefr (𝑅 We 𝐴𝑅 Fr 𝐴)

Proof of Theorem wefr
StepHypRef Expression
1 df-we 5065 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 476 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5024   Fr wfr 5060   We wwe 5062
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 197  df-an 386  df-we 5065
This theorem is referenced by:  wefrc  5098  wereu  5100  wereu2  5101  ordfr  5726  wexp  7276  wfrlem14  7413  wofib  8435  wemapso  8441  wemapso2lem  8442  cflim2  9070  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwe2  9450  welb  33502  fnwe2lem2  37440  onfrALTlem3  38579  onfrALTlem3VD  38943
  Copyright terms: Public domain W3C validator