![]() |
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 7476. (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 5477 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5475 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5437 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 399 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 209 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5495 wess 5506 weeq1 5507 weeq2 5508 wefr 5509 weso 5510 we0 5514 weinxp 5600 wesn 5604 isowe 7081 isowe2 7082 dfwe2 7476 wexp 7807 wofi 8751 dford5reg 33140 finorwe 34799 fin2so 35044 |
Copyright terms: Public domain | W3C validator |