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

Theorem weeq1 5654
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 5636 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5599 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 630 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5623 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5623 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 314 1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533   Or wor 5577   Fr wfr 5618   We wwe 5620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-ex 1774  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-br 5139  df-po 5578  df-so 5579  df-fr 5621  df-we 5623
This theorem is referenced by:  oieq1  9503  hartogslem1  9533  wemapwe  9688  infxpenlem  10004  dfac8b  10022  ac10ct  10025  fpwwe2cbv  10621  fpwwe2lem2  10623  fpwwe2lem4  10625  fpwwecbv  10635  fpwwelem  10636  canthnumlem  10639  canthwelem  10641  canthwe  10642  canthp1lem2  10644  pwfseqlem4a  10652  pwfseqlem4  10653  ltbwe  21909  vitali  25464  fin2so  36965  weeq12d  42271  dnwech  42279  aomclem5  42289  aomclem6  42290  aomclem7  42291
  Copyright terms: Public domain W3C validator