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

Theorem weeq1 4872
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
Assertion
Ref Expression
weeq1

Proof of Theorem weeq1
StepHypRef Expression
1 freq1 4854 . . 3
2 soeq1 4824 . . 3
31, 2anbi12d 710 . 2
4 df-we 4845 . 2
5 df-we 4845 . 2
63, 4, 53bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  Orwor 4804  Frwfr 4840  Wewwe 4842
This theorem is referenced by:  oieq1  7958  hartogslem1  7988  wemapwe  8160  wemapweOLD  8161  infxpenlem  8412  dfac8b  8433  ac10ct  8436  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwe2lem5  9033  fpwwecbv  9043  fpwwelem  9044  canthnumlem  9047  canthwelem  9049  canthwe  9050  canthp1lem2  9052  pwfseqlem4a  9060  pwfseqlem4  9061  ltbwe  18137  vitali  22022  fin2so  30040  weeq12d  30985  dnwech  30994  aomclem5  31004  aomclem6  31005  aomclem7  31006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-ex 1613  df-cleq 2449  df-clel 2452  df-ral 2812  df-rex 2813  df-br 4453  df-po 4805  df-so 4806  df-fr 4843  df-we 4845
  Copyright terms: Public domain W3C validator