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

Theorem weeq1 4822
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 4804 . . 3  |-  ( R  =  S  ->  ( R  Fr  A  <->  S  Fr  A ) )
2 soeq1 4774 . . 3  |-  ( R  =  S  ->  ( R  Or  A  <->  S  Or  A ) )
31, 2anbi12d 717 . 2  |-  ( R  =  S  ->  (
( R  Fr  A  /\  R  Or  A
)  <->  ( S  Fr  A  /\  S  Or  A
) ) )
4 df-we 4795 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
5 df-we 4795 . 2  |-  ( S  We  A  <->  ( S  Fr  A  /\  S  Or  A ) )
63, 4, 53bitr4g 292 1  |-  ( R  =  S  ->  ( R  We  A  <->  S  We  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444    Or wor 4754    Fr wfr 4790    We wwe 4792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-ex 1664  df-cleq 2444  df-clel 2447  df-ral 2742  df-rex 2743  df-br 4403  df-po 4755  df-so 4756  df-fr 4793  df-we 4795
This theorem is referenced by:  oieq1  8027  hartogslem1  8057  wemapwe  8202  infxpenlem  8444  dfac8b  8462  ac10ct  8465  fpwwe2cbv  9055  fpwwe2lem2  9057  fpwwe2lem5  9059  fpwwecbv  9069  fpwwelem  9070  canthnumlem  9073  canthwelem  9075  canthwe  9076  canthp1lem2  9078  pwfseqlem4a  9086  pwfseqlem4  9087  ltbwe  18696  vitali  22571  fin2so  31932  weeq12d  35898  dnwech  35906  aomclem5  35916  aomclem6  35917  aomclem7  35918
  Copyright terms: Public domain W3C validator