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

Theorem wefr 5394
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 5365 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 490 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5322   Fr wfr 5360   We wwe 5362
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 199  df-an 388  df-we 5365
This theorem is referenced by:  wefrc  5398  wereu  5400  wereu2  5401  ordfr  6042  wexp  7628  wfrlem14  7771  wofib  8803  wemapso  8809  wemapso2lem  8810  cflim2  9482  fpwwe2lem12  9860  fpwwe2lem13  9861  fpwwe2  9862  welb  34486  fnwe2lem2  39081  onfrALTlem3  40331  onfrALTlem3VD  40674
  Copyright terms: Public domain W3C validator