Theorem wefr 5104

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

Syntax hints:   → wi 4   Or wor 5034   Fr wfr 5070   We wwe 5072

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 386  df-we 5075

This theorem is referenced by:  wefrc  5108  wereu  5110  wereu2  5111  ordfr  5738  wexp  7291  wfrlem14  7428  wofib  8450  wemapso  8456  wemapso2lem  8457  cflim2  9085  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  welb  33531  fnwe2lem2  37621  onfrALTlem3  38759  onfrALTlem3VD  39123