Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > weeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
weeq2 | ⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | freq2 5560 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) | |
2 | soeq2 5525 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | |
3 | 1, 2 | anbi12d 631 | . 2 ⊢ (𝐴 = 𝐵 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))) |
4 | df-we 5546 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
5 | df-we 5546 | . 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 396 = wceq 1539 Or wor 5502 Fr wfr 5541 We wwe 5543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-v 3434 df-in 3894 df-ss 3904 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 |
This theorem is referenced by: ordeq 6273 0we1 8336 oieq2 9272 hartogslem1 9301 wemapwe 9455 ween 9791 dfac8 9891 weth 10251 fpwwe2cbv 10386 fpwwe2lem2 10388 fpwwe2lem4 10390 fpwwecbv 10400 fpwwelem 10401 canthwelem 10406 canthwe 10407 pwfseqlem4a 10417 pwfseqlem4 10418 ltweuz 13681 ltwenn 13682 bpolylem 15758 ltbwe 21245 vitali 24777 weeq12d 40865 aomclem6 40884 omeiunle 44055 |
Copyright terms: Public domain | W3C validator |