MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  weeq1 Structured version   Visualization version   GIF version

Theorem weeq1 5064
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
Assertion
Ref Expression
weeq1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))

Proof of Theorem weeq1
StepHypRef Expression
1 freq1 5046 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5016 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 746 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5037 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5037 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 303 1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480   Or wor 4996   Fr wfr 5032   We wwe 5034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-ex 1702  df-cleq 2614  df-clel 2617  df-ral 2912  df-rex 2913  df-br 4616  df-po 4997  df-so 4998  df-fr 5035  df-we 5037
This theorem is referenced by:  oieq1  8364  hartogslem1  8394  wemapwe  8541  infxpenlem  8783  dfac8b  8801  ac10ct  8804  fpwwe2cbv  9399  fpwwe2lem2  9401  fpwwe2lem5  9403  fpwwecbv  9413  fpwwelem  9414  canthnumlem  9417  canthwelem  9419  canthwe  9420  canthp1lem2  9422  pwfseqlem4a  9430  pwfseqlem4  9431  ltbwe  19394  vitali  23295  fin2so  33049  weeq12d  37111  dnwech  37119  aomclem5  37129  aomclem6  37130  aomclem7  37131
  Copyright terms: Public domain W3C validator