Theorem weeq1 5102

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)

Assertion

Ref	Expression
weeq1	|- ( R = S -> ( R We A <-> S We A ) )

Proof of Theorem weeq1

Step	Hyp	Ref	Expression
1		freq1 5084	. . 3 |- ( R = S -> ( R Fr A <-> S Fr A ) )
2		soeq1 5054	. . 3 |- ( R = S -> ( R Or A <-> S Or A ) )
3	1, 2	anbi12d 747	. 2 |- ( R = S -> ( ( R Fr A /\ R Or A ) <-> ( S Fr A /\ S Or A ) ) )
4		df-we 5075	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
5		df-we 5075	. 2 |- ( S We A <-> ( S Fr A /\ S Or A ) )
6	3, 4, 5	3bitr4g 303	1 |- ( R = S -> ( R We A <-> S We A ) )

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-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-ex 1705  df-cleq 2615  df-clel 2618  df-ral 2917  df-rex 2918  df-br 4654  df-po 5035  df-so 5036  df-fr 5073  df-we 5075

This theorem is referenced by:  oieq1  8417  hartogslem1  8447  wemapwe  8594  infxpenlem  8836  dfac8b  8854  ac10ct  8857  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwe2lem5  9456  fpwwecbv  9466  fpwwelem  9467  canthnumlem  9470  canthwelem  9472  canthwe  9473  canthp1lem2  9475  pwfseqlem4a  9483  pwfseqlem4  9484  ltbwe  19472  vitali  23382  fin2so  33396  weeq12d  37610  dnwech  37618  aomclem5  37628  aomclem6  37629  aomclem7  37630