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

Theorem weeq2 4799
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
weeq2  |-  ( A  =  B  ->  ( R  We  A  <->  R  We  B ) )

Proof of Theorem weeq2
StepHypRef Expression
1 freq2 4781 . . 3  |-  ( A  =  B  ->  ( R  Fr  A  <->  R  Fr  B ) )
2 soeq2 4751 . . 3  |-  ( A  =  B  ->  ( R  Or  A  <->  R  Or  B ) )
31, 2anbi12d 708 . 2  |-  ( A  =  B  ->  (
( R  Fr  A  /\  R  Or  A
)  <->  ( R  Fr  B  /\  R  Or  B
) ) )
4 df-we 4771 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
5 df-we 4771 . 2  |-  ( R  We  B  <->  ( R  Fr  B  /\  R  Or  B ) )
63, 4, 53bitr4g 288 1  |-  ( A  =  B  ->  ( R  We  A  <->  R  We  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    Or wor 4730    Fr wfr 4766    We wwe 4768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-ral 2751  df-in 3413  df-ss 3420  df-po 4731  df-so 4732  df-fr 4769  df-we 4771
This theorem is referenced by:  ordeq  4816  0we1  7096  oieq2  7875  hartogslem1  7904  wemapwe  8074  wemapweOLD  8075  ween  8351  dfac8  8450  weth  8810  fpwwe2cbv  8941  fpwwe2lem2  8943  fpwwe2lem5  8945  fpwwecbv  8955  fpwwelem  8956  canthwelem  8961  canthwe  8962  pwfseqlem4a  8972  pwfseqlem4  8973  ltweuz  11998  ltwenn  11999  ltbwe  18273  vitali  22130  bpolylem  30003  weeq12d  31191  aomclem6  31211
  Copyright terms: Public domain W3C validator