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

Theorem wefr 5668
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 5635 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 496 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5589   Fr wfr 5630   We wwe 5632
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 206  df-an 395  df-we 5635
This theorem is referenced by:  wefrc  5672  wereu  5674  wereu2  5675  tz6.26  6355  wfi  6358  wfisg  6361  wfis2fg  6364  ordfr  6386  wexp  8135  wfrlem14OLD  8343  wfrfun  8353  wfrresex  8354  wfr2a  8355  wfr1  8356  wofib  9570  wemapso  9576  wemapso2lem  9577  cflim2  10288  fpwwe2lem11  10666  fpwwe2lem12  10667  fpwwe2  10668  welb  37340  fnwe2lem2  42617  onfrALTlem3  44125  onfrALTlem3VD  44468
  Copyright terms: Public domain W3C validator