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 7496. (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 5513 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5511 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5473 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 398 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 208 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5531 wess 5542 weeq1 5543 weeq2 5544 wefr 5545 weso 5546 we0 5550 weinxp 5636 wesn 5640 isowe 7102 isowe2 7103 dfwe2 7496 wexp 7824 wofi 8767 dford5reg 33027 finorwe 34666 fin2so 34894 |
Copyright terms: Public domain | W3C validator |