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 6981. (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 5072 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5070 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5034 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 384 | . 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 5090 wess 5101 weeq1 5102 weeq2 5103 wefr 5104 weso 5105 we0 5109 weinxp 5186 wesn 5190 isowe 6599 isowe2 6600 dfwe2 6981 wexp 7291 wofi 8209 dford5reg 31687 fin2so 33396 |
Copyright terms: Public domain | W3C validator |