Theorem wefr 5028

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 4999	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simplbi 475	1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Syntax hints:   → wi 4   Or wor 4958   Fr wfr 4994   We wwe 4996

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 196  df-an 385  df-we 4999

This theorem is referenced by:  wefrc  5032  wereu  5034  wereu2  5035  ordfr  5655  wexp  7178  wfrlem14  7315  wofib  8333  wemapso  8339  wemapso2lem  8340  cflim2  8968  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  welb  32701  fnwe2lem2  36639  onfrALTlem3  37780  onfrALTlem3VD  38145