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 496	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  6311  wfi  6313  wfisg  6315  wfis2fg  6317  ordfr  6338  wexp  8080  wfrfun  8273  wfrresex  8274  wfr2a  8275  wfr1  8276  wofib  9460  wemapso  9466  wemapso2lem  9467  cflim2  10185  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  ons2ind  28267  weiunwe  36651  welb  38057  fnwe2lem2  43479  onfrALTlem3  44971  onfrALTlem3VD  45313