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

Theorem weeq2 4818
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 4800 . . 3  |-  ( A  =  B  ->  ( R  Fr  A  <->  R  Fr  B ) )
2 soeq2 4770 . . 3  |-  ( A  =  B  ->  ( R  Or  A  <->  R  Or  B ) )
31, 2anbi12d 710 . 2  |-  ( A  =  B  ->  (
( R  Fr  A  /\  R  Or  A
)  <->  ( R  Fr  B  /\  R  Or  B
) ) )
4 df-we 4790 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
5 df-we 4790 . 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 369    = wceq 1370    Or wor 4749    Fr wfr 4785    We wwe 4787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-in 3444  df-ss 3451  df-po 4750  df-so 4751  df-fr 4788  df-we 4790
This theorem is referenced by:  ordeq  4835  0we1  7057  oieq2  7839  hartogslem1  7868  wemapwe  8040  wemapweOLD  8041  ween  8317  dfac8  8416  weth  8776  fpwwe2cbv  8909  fpwwe2lem2  8911  fpwwe2lem5  8913  fpwwecbv  8923  fpwwelem  8924  canthwelem  8929  canthwe  8930  pwfseqlem4a  8940  pwfseqlem4  8941  ltweuz  11902  ltwenn  11903  ltbwe  17679  vitali  21227  bpolylem  28336  weeq12d  29541  aomclem6  29561
  Copyright terms: Public domain W3C validator