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

Theorem weeq1 5345
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 5327 . . 3 (𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
2 soeq1 5296 . . 3 (𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
31, 2anbi12d 624 . 2 (𝑅 = 𝑆 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴)))
4 df-we 5318 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5318 . 2 (𝑆 We 𝐴 ↔ (𝑆 Fr 𝐴𝑆 Or 𝐴))
63, 4, 53bitr4g 306 1 (𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601   Or wor 5275   Fr wfr 5313   We wwe 5315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-ex 1824  df-cleq 2770  df-clel 2774  df-ral 3095  df-rex 3096  df-br 4889  df-po 5276  df-so 5277  df-fr 5316  df-we 5318
This theorem is referenced by:  oieq1  8708  hartogslem1  8738  wemapwe  8893  infxpenlem  9171  dfac8b  9189  ac10ct  9192  fpwwe2cbv  9789  fpwwe2lem2  9791  fpwwe2lem5  9793  fpwwecbv  9803  fpwwelem  9804  canthnumlem  9807  canthwelem  9809  canthwe  9810  canthp1lem2  9812  pwfseqlem4a  9820  pwfseqlem4  9821  ltbwe  19880  vitali  23828  fin2so  34030  weeq12d  38583  dnwech  38591  aomclem5  38601  aomclem6  38602  aomclem7  38603
  Copyright terms: Public domain W3C validator