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

Theorem wefr 5675
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 5639 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 497 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5591   Fr wfr 5634   We wwe 5636
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 207  df-an 396  df-we 5639
This theorem is referenced by:  wefrc  5679  wereu  5681  wereu2  5682  tz6.26  6368  wfi  6371  wfisg  6374  wfis2fg  6377  ordfr  6399  wexp  8155  wfrlem14OLD  8362  wfrfun  8372  wfrresex  8373  wfr2a  8374  wfr1  8375  wofib  9585  wemapso  9591  wemapso2lem  9592  cflim2  10303  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  weiunwe  36470  welb  37743  fnwe2lem2  43063  onfrALTlem3  44564  onfrALTlem3VD  44907
  Copyright terms: Public domain W3C validator