| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > wefr | Structured version Visualization version GIF version | ||
| Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.) |
| Ref | Expression |
|---|---|
| wefr | ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-we 5639 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Or wor 5591 Fr wfr 5634 We wwe 5636 |
| 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 5639 |
| This theorem is referenced by: wefrc 5679 wereu 5681 wereu2 5682 tz6.26 6368 wfi 6371 wfisg 6374 wfis2fg 6377 ordfr 6399 wexp 8155 wfrlem14OLD 8362 wfrfun 8372 wfrresex 8373 wfr2a 8374 wfr1 8375 wofib 9585 wemapso 9591 wemapso2lem 9592 cflim2 10303 fpwwe2lem11 10681 fpwwe2lem12 10682 fpwwe2 10683 weiunwe 36470 welb 37743 fnwe2lem2 43063 onfrALTlem3 44564 onfrALTlem3VD 44907 |
| Copyright terms: Public domain | W3C validator |