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

Step	Hyp	Ref	Expression
1		freq2 4855	. . 3
2		soeq2 4825	. . 3
3	1, 2	anbi12d 710	. 2
4		df-we 4845	. 2
5		df-we 4845	. 2
6	3, 4, 5	3bitr4g 288	1

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