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

Theorem weeq1 5514
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 5496 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5464 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 634 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5486 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5486 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 317 1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542   Or wor 5442   Fr wfr 5481   We wwe 5483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-ex 1787  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-br 5032  df-po 5443  df-so 5444  df-fr 5484  df-we 5486
This theorem is referenced by:  oieq1  9052  hartogslem1  9082  wemapwe  9236  infxpenlem  9516  dfac8b  9534  ac10ct  9537  fpwwe2cbv  10133  fpwwe2lem2  10135  fpwwe2lem4  10137  fpwwecbv  10147  fpwwelem  10148  canthnumlem  10151  canthwelem  10153  canthwe  10154  canthp1lem2  10156  pwfseqlem4a  10164  pwfseqlem4  10165  ltbwe  20858  vitali  24368  fin2so  35410  weeq12d  40460  dnwech  40468  aomclem5  40478  aomclem6  40479  aomclem7  40480
  Copyright terms: Public domain W3C validator