![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > weeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
weeq1 | ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | freq1 5636 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | |
2 | soeq1 5599 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | |
3 | 1, 2 | anbi12d 630 | . 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))) |
4 | df-we 5623 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
5 | df-we 5623 | . 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 Or wor 5577 Fr wfr 5618 We wwe 5620 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-ex 1774 df-cleq 2716 df-clel 2802 df-ral 3054 df-rex 3063 df-br 5139 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 |
This theorem is referenced by: oieq1 9503 hartogslem1 9533 wemapwe 9688 infxpenlem 10004 dfac8b 10022 ac10ct 10025 fpwwe2cbv 10621 fpwwe2lem2 10623 fpwwe2lem4 10625 fpwwecbv 10635 fpwwelem 10636 canthnumlem 10639 canthwelem 10641 canthwe 10642 canthp1lem2 10644 pwfseqlem4a 10652 pwfseqlem4 10653 ltbwe 21909 vitali 25464 fin2so 36965 weeq12d 42271 dnwech 42279 aomclem5 42289 aomclem6 42290 aomclem7 42291 |
Copyright terms: Public domain | W3C validator |