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 5496 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | |
2 | soeq1 5464 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | |
3 | 1, 2 | anbi12d 634 | . 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))) |
4 | df-we 5486 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
5 | df-we 5486 | . 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)) | |
6 | 3, 4, 5 | 3bitr4g 317 | 1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 Or wor 5442 Fr wfr 5481 We wwe 5483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-ex 1787 df-cleq 2731 df-clel 2812 df-ral 3059 df-rex 3060 df-br 5032 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 |
This theorem is referenced by: oieq1 9052 hartogslem1 9082 wemapwe 9236 infxpenlem 9516 dfac8b 9534 ac10ct 9537 fpwwe2cbv 10133 fpwwe2lem2 10135 fpwwe2lem4 10137 fpwwecbv 10147 fpwwelem 10148 canthnumlem 10151 canthwelem 10153 canthwe 10154 canthp1lem2 10156 pwfseqlem4a 10164 pwfseqlem4 10165 ltbwe 20858 vitali 24368 fin2so 35410 weeq12d 40460 dnwech 40468 aomclem5 40478 aomclem6 40479 aomclem7 40480 |
Copyright terms: Public domain | W3C validator |