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 6873. (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 4996 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 4994 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 4958 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 383 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 195 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5014 wess 5025 weeq1 5026 weeq2 5027 wefr 5028 weso 5029 we0 5033 weinxp 5109 wesn 5113 isowe 6499 isowe2 6500 dfwe2 6873 wexp 7178 wofi 8094 dford5reg 30931 fin2so 32566 |
Copyright terms: Public domain | W3C validator |