Theorem weeq1 4822

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 4804	. . 3 |- ( R = S -> ( R Fr A <-> S Fr A ) )
2		soeq1 4774	. . 3 |- ( R = S -> ( R Or A <-> S Or A ) )
3	1, 2	anbi12d 717	. 2 |- ( R = S -> ( ( R Fr A /\ R Or A ) <-> ( S Fr A /\ S Or A ) ) )
4		df-we 4795	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
5		df-we 4795	. 2 |- ( S We A <-> ( S Fr A /\ S Or A ) )
6	3, 4, 5	3bitr4g 292	1 |- ( R = S -> ( R We A <-> S We A ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   Or wor 4754   Fr wfr 4790   We wwe 4792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-ex 1664  df-cleq 2444  df-clel 2447  df-ral 2742  df-rex 2743  df-br 4403  df-po 4755  df-so 4756  df-fr 4793  df-we 4795

This theorem is referenced by:  oieq1  8027  hartogslem1  8057  wemapwe  8202  infxpenlem  8444  dfac8b  8462  ac10ct  8465  fpwwe2cbv  9055  fpwwe2lem2  9057  fpwwe2lem5  9059  fpwwecbv  9069  fpwwelem  9070  canthnumlem  9073  canthwelem  9075  canthwe  9076  canthp1lem2  9078  pwfseqlem4a  9086  pwfseqlem4  9087  ltbwe  18696  vitali  22571  fin2so  31932  weeq12d  35898  dnwech  35906  aomclem5  35916  aomclem6  35917  aomclem7  35918