![]() |
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 5327 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | |
2 | soeq1 5296 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | |
3 | 1, 2 | anbi12d 624 | . 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))) |
4 | df-we 5318 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
5 | df-we 5318 | . 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)) | |
6 | 3, 4, 5 | 3bitr4g 306 | 1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 Or wor 5275 Fr wfr 5313 We wwe 5315 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-ex 1824 df-cleq 2770 df-clel 2774 df-ral 3095 df-rex 3096 df-br 4889 df-po 5276 df-so 5277 df-fr 5316 df-we 5318 |
This theorem is referenced by: oieq1 8708 hartogslem1 8738 wemapwe 8893 infxpenlem 9171 dfac8b 9189 ac10ct 9192 fpwwe2cbv 9789 fpwwe2lem2 9791 fpwwe2lem5 9793 fpwwecbv 9803 fpwwelem 9804 canthnumlem 9807 canthwelem 9809 canthwe 9810 canthp1lem2 9812 pwfseqlem4a 9820 pwfseqlem4 9821 ltbwe 19880 vitali 23828 fin2so 34030 weeq12d 38583 dnwech 38591 aomclem5 38601 aomclem6 38602 aomclem7 38603 |
Copyright terms: Public domain | W3C validator |