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

Theorem weeq2 4873
 Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
weeq2

Proof of Theorem weeq2
StepHypRef Expression
1 freq2 4855 . . 3
2 soeq2 4825 . . 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:  ordeq  4890  0we1  7175  oieq2  7959  hartogslem1  7988  wemapwe  8160  wemapweOLD  8161  ween  8437  dfac8  8536  weth  8896  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwe2lem5  9033  fpwwecbv  9043  fpwwelem  9044  canthwelem  9049  canthwe  9050  pwfseqlem4a  9060  pwfseqlem4  9061  ltweuz  12072  ltwenn  12073  ltbwe  18137  vitali  22022  bpolylem  29810  weeq12d  30985  aomclem6  31005 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-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-in 3482  df-ss 3489  df-po 4805  df-so 4806  df-fr 4843  df-we 4845
 Copyright terms: Public domain W3C validator