![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-we | Structured version Visualization version GIF version |
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7765. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
df-we | ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | wwe 5630 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5628 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5587 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 395 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 205 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5652 wess 5663 weeq1 5664 weeq2 5665 wefr 5666 weso 5667 we0 5671 weinxp 5760 wesn 5764 isowe 7349 isowe2 7350 dfwe2 7765 epweon 7766 wexp 8121 wofi 9298 dford5reg 35224 finorwe 36727 fin2so 36939 |
Copyright terms: Public domain | W3C validator |