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

Theorem weeq1 5542
 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 5524 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5493 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 632 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5515 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5515 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 316 1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   Or wor 5472   Fr wfr 5510   We wwe 5512 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144  df-br 5066  df-po 5473  df-so 5474  df-fr 5513  df-we 5515 This theorem is referenced by:  oieq1  8975  hartogslem1  9005  wemapwe  9159  infxpenlem  9438  dfac8b  9456  ac10ct  9459  fpwwe2cbv  10051  fpwwe2lem2  10053  fpwwe2lem5  10055  fpwwecbv  10065  fpwwelem  10066  canthnumlem  10069  canthwelem  10071  canthwe  10072  canthp1lem2  10074  pwfseqlem4a  10082  pwfseqlem4  10083  ltbwe  20252  vitali  24213  fin2so  34878  weeq12d  39638  dnwech  39646  aomclem5  39656  aomclem6  39657  aomclem7  39658
 Copyright terms: Public domain W3C validator