| 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 7794. (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 5636 | . 2 wff 𝑅 We 𝐴 |
| 4 | 1, 2 | wfr 5634 | . . 3 wff 𝑅 Fr 𝐴 |
| 5 | 1, 2 | wor 5591 | . . 3 wff 𝑅 Or 𝐴 |
| 6 | 4, 5 | wa 395 | . 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) |
| 7 | 3, 6 | wb 206 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: nfwe 5660 wess 5671 weeq1 5672 weeq2 5673 wefr 5675 weso 5676 we0 5680 weinxp 5770 wesn 5774 isowe 7369 isowe2 7370 dfwe2 7794 epweon 7795 wexp 8155 wofi 9325 dford5reg 35783 weiunwe 36470 finorwe 37383 fin2so 37614 |
| Copyright terms: Public domain | W3C validator |