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 5559 | . . 3 ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | |
2 | soeq1 5524 | . . 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-or 845 df-3or 1087 df-ex 1783 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-br 5075 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 |
This theorem is referenced by: oieq1 9271 hartogslem1 9301 wemapwe 9455 infxpenlem 9769 dfac8b 9787 ac10ct 9790 fpwwe2cbv 10386 fpwwe2lem2 10388 fpwwe2lem4 10390 fpwwecbv 10400 fpwwelem 10401 canthnumlem 10404 canthwelem 10406 canthwe 10407 canthp1lem2 10409 pwfseqlem4a 10417 pwfseqlem4 10418 ltbwe 21245 vitali 24777 fin2so 35764 weeq12d 40865 dnwech 40873 aomclem5 40883 aomclem6 40884 aomclem7 40885 |
Copyright terms: Public domain | W3C validator |