![]() |
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 7023. (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 5101 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5099 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5063 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 383 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 196 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5119 wess 5130 weeq1 5131 weeq2 5132 wefr 5133 weso 5134 we0 5138 weinxp 5220 wesn 5224 isowe 6639 isowe2 6640 dfwe2 7023 wexp 7336 wofi 8250 dford5reg 31811 fin2so 33526 |
Copyright terms: Public domain | W3C validator |