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

Theorem wefr 5028
 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 4999 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 475 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   Or wor 4958   Fr wfr 4994   We wwe 4996 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 196  df-an 385  df-we 4999 This theorem is referenced by:  wefrc  5032  wereu  5034  wereu2  5035  ordfr  5655  wexp  7178  wfrlem14  7315  wofib  8333  wemapso  8339  wemapso2lem  8340  cflim2  8968  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  welb  32701  fnwe2lem2  36639  onfrALTlem3  37780  onfrALTlem3VD  38145
 Copyright terms: Public domain W3C validator