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

Theorem weeq1 5577
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 5559 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5524 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 631 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5546 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5546 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 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