Theorem weeq2 5103

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

Step	Hyp	Ref	Expression
1		freq2 5085	. . 3 |- ( A = B -> ( R Fr A <-> R Fr B ) )
2		soeq2 5055	. . 3 |- ( A = B -> ( R Or A <-> R Or B ) )
3	1, 2	anbi12d 747	. 2 |- ( A = B -> ( ( R Fr A /\ R Or A ) <-> ( R Fr B /\ R Or B ) ) )
4		df-we 5075	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
5		df-we 5075	. 2 |- ( R We B <-> ( R Fr B /\ R Or B ) )
6	3, 4, 5	3bitr4g 303	1 |- ( A = B -> ( R We A <-> R We B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   Or wor 5034   Fr wfr 5070   We wwe 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-in 3581  df-ss 3588  df-po 5035  df-so 5036  df-fr 5073  df-we 5075

This theorem is referenced by:  ordeq  5730  0we1  7586  oieq2  8418  hartogslem1  8447  wemapwe  8594  ween  8858  dfac8  8957  weth  9317  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwe2lem5  9456  fpwwecbv  9466  fpwwelem  9467  canthwelem  9472  canthwe  9473  pwfseqlem4a  9483  pwfseqlem4  9484  ltweuz  12760  ltwenn  12761  bpolylem  14779  ltbwe  19472  vitali  23382  weeq12d  37610  aomclem6  37629  omeiunle  40731