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

Theorem weeq1 5026
 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 5008 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 4978 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 743 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 4999 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 4999 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 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