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

Theorem wefr 5239
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 5210 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simplbi 485 1 (𝑅 We 𝐴𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5169   Fr wfr 5205   We wwe 5207
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 197  df-an 383  df-we 5210
This theorem is referenced by:  wefrc  5243  wereu  5245  wereu2  5246  ordfr  5881  wexp  7442  wfrlem14  7581  wofib  8606  wemapso  8612  wemapso2lem  8613  cflim2  9287  fpwwe2lem12  9665  fpwwe2lem13  9666  fpwwe2  9667  welb  33863  fnwe2lem2  38147  onfrALTlem3  39284  onfrALTlem3VD  39645
  Copyright terms: Public domain W3C validator