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

Theorem wefr 5513
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 5484 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 501 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5441   Fr wfr 5479   We wwe 5481
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 210  df-an 400  df-we 5484
This theorem is referenced by:  wefrc  5517  wereu  5519  wereu2  5520  ordfr  6178  wexp  7811  wfrlem14  7955  wofib  8997  wemapso  9003  wemapso2lem  9004  cflim2  9678  fpwwe2lem12  10056  fpwwe2lem13  10057  fpwwe2  10058  welb  35167  fnwe2lem2  39982  onfrALTlem3  41237  onfrALTlem3VD  41580
  Copyright terms: Public domain W3C validator