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

Theorem weeq1 4713
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 4695 . . 3  |-  ( R  =  S  ->  ( R  Fr  A  <->  S  Fr  A ) )
2 soeq1 4665 . . 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 4686 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
5 df-we 4686 . 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 1369    Or wor 4645    Fr wfr 4681    We wwe 4683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-ral 2725  df-rex 2726  df-br 4298  df-po 4646  df-so 4647  df-fr 4684  df-we 4686
This theorem is referenced by:  oieq1  7731  hartogslem1  7761  wemapwe  7933  wemapweOLD  7934  infxpenlem  8185  dfac8b  8206  ac10ct  8209  fpwwe2cbv  8802  fpwwe2lem2  8804  fpwwe2lem5  8806  fpwwecbv  8816  fpwwelem  8817  canthnumlem  8820  canthwelem  8822  canthwe  8823  canthp1lem2  8825  pwfseqlem4a  8833  pwfseqlem4  8834  ltbwe  17559  vitali  21098  fin2so  28421  weeq12d  29397  dnwech  29406  aomclem5  29416  aomclem6  29417  aomclem7  29418
  Copyright terms: Public domain W3C validator