Theorem wefr 5621

Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)

Assertion

Ref	Expression
wefr	⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Proof of Theorem wefr

Step	Hyp	Ref	Expression
1		df-we 5586	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simplbi 497	1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Syntax hints:   → wi 4   Or wor 5538   Fr wfr 5581   We wwe 5583

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 5586

This theorem is referenced by:  wefrc  5625  wereu  5627  wereu2  5628  tz6.26  6308  wfi  6310  wfisg  6312  wfis2fg  6314  ordfr  6335  wexp  8086  wfrfun  8279  wfrresex  8280  wfr2a  8281  wfr1  8282  wofib  9474  wemapso  9480  wemapso2lem  9481  cflim2  10192  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  weiunwe  36450  welb  37723  fnwe2lem2  43033  onfrALTlem3  44527  onfrALTlem3VD  44869