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 5008 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | |
2 | soeq1 4978 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | |
3 | 1, 2 | anbi12d 743 | . 2 ⊢ (𝑅 = 𝑆 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴))) |
4 | df-we 4999 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
5 | df-we 4999 | . 2 ⊢ (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴 ∧ 𝑆 Or 𝐴)) | |
6 | 3, 4, 5 | 3bitr4g 302 | 1 ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 Or wor 4958 Fr wfr 4994 We wwe 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-ex 1696 df-cleq 2603 df-clel 2606 df-ral 2901 df-rex 2902 df-br 4584 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 |
This theorem is referenced by: oieq1 8300 hartogslem1 8330 wemapwe 8477 infxpenlem 8719 dfac8b 8737 ac10ct 8740 fpwwe2cbv 9331 fpwwe2lem2 9333 fpwwe2lem5 9335 fpwwecbv 9345 fpwwelem 9346 canthnumlem 9349 canthwelem 9351 canthwe 9352 canthp1lem2 9354 pwfseqlem4a 9362 pwfseqlem4 9363 ltbwe 19293 vitali 23188 fin2so 32566 weeq12d 36628 dnwech 36636 aomclem5 36646 aomclem6 36647 aomclem7 36648 |
Copyright terms: Public domain | W3C validator |