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

Theorem weeq1 4876
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
Assertion
Ref Expression
weeq1  |-  ( R  =  S  ->  ( R  We  A  <->  S  We  A ) )

Proof of Theorem weeq1
StepHypRef Expression
1 freq1 4858 . . 3  |-  ( R  =  S  ->  ( R  Fr  A  <->  S  Fr  A ) )
2 soeq1 4828 . . 3  |-  ( R  =  S  ->  ( R  Or  A  <->  S  Or  A ) )
31, 2anbi12d 710 . 2  |-  ( R  =  S  ->  (
( R  Fr  A  /\  R  Or  A
)  <->  ( S  Fr  A  /\  S  Or  A
) ) )
4 df-we 4849 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
5 df-we 4849 . 2  |-  ( S  We  A  <->  ( S  Fr  A  /\  S  Or  A ) )
63, 4, 53bitr4g 288 1  |-  ( R  =  S  ->  ( R  We  A  <->  S  We  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395    Or wor 4808    Fr wfr 4844    We wwe 4846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-ex 1614  df-cleq 2449  df-clel 2452  df-ral 2812  df-rex 2813  df-br 4457  df-po 4809  df-so 4810  df-fr 4847  df-we 4849
This theorem is referenced by:  oieq1  7955  hartogslem1  7985  wemapwe  8156  wemapweOLD  8157  infxpenlem  8408  dfac8b  8429  ac10ct  8432  fpwwe2cbv  9025  fpwwe2lem2  9027  fpwwe2lem5  9029  fpwwecbv  9039  fpwwelem  9040  canthnumlem  9043  canthwelem  9045  canthwe  9046  canthp1lem2  9048  pwfseqlem4a  9056  pwfseqlem4  9057  ltbwe  18264  vitali  22148  fin2so  30245  weeq12d  31189  dnwech  31198  aomclem5  31208  aomclem6  31209  aomclem7  31210
  Copyright terms: Public domain W3C validator