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 7484. (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 5507 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5505 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5467 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 396 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 207 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5525 wess 5536 weeq1 5537 weeq2 5538 wefr 5539 weso 5540 we0 5544 weinxp 5630 wesn 5634 isowe 7091 isowe2 7092 dfwe2 7484 wexp 7815 wofi 8756 dford5reg 32925 finorwe 34546 fin2so 34761 |
Copyright terms: Public domain | W3C validator |