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 7515. (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 5482 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 5480 | . . 3 wff 𝑅 Fr 𝐴 |
5 | 1, 2 | wor 5441 | . . 3 wff 𝑅 Or 𝐴 |
6 | 4, 5 | wa 399 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
7 | 3, 6 | wb 209 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: nfwe 5501 wess 5512 weeq1 5513 weeq2 5514 wefr 5515 weso 5516 we0 5520 weinxp 5607 wesn 5611 isowe 7115 isowe2 7116 dfwe2 7515 wexp 7850 wofi 8841 dford5reg 33330 finorwe 35176 fin2so 35387 |
Copyright terms: Public domain | W3C validator |