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

Step	Hyp	Ref	Expression
1		freq1 4854	. . 3
2		soeq1 4824	. . 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:  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