Theorem weeq1 4876

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 4858	. . 3 |- ( R = S -> ( R Fr A <-> S Fr A ) )
2		soeq1 4828	. . 3 |- ( R = S -> ( R Or A <-> S Or A ) )
3	1, 2	anbi12d 710	. 2 |- ( R = S -> ( ( R Fr A /\ R Or A ) <-> ( S Fr A /\ S Or A ) ) )
4		df-we 4849	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
5		df-we 4849	. 2 |- ( S We A <-> ( S Fr A /\ S Or A ) )
6	3, 4, 5	3bitr4g 288	1 |- ( R = S -> ( R We A <-> S We A ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1395   Or wor 4808   Fr wfr 4844   We wwe 4846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-ex 1614  df-cleq 2449  df-clel 2452  df-ral 2812  df-rex 2813  df-br 4457  df-po 4809  df-so 4810  df-fr 4847  df-we 4849

This theorem is referenced by:  oieq1  7955  hartogslem1  7985  wemapwe  8156  wemapweOLD  8157  infxpenlem  8408  dfac8b  8429  ac10ct  8432  fpwwe2cbv  9025  fpwwe2lem2  9027  fpwwe2lem5  9029  fpwwecbv  9039  fpwwelem  9040  canthnumlem  9043  canthwelem  9045  canthwe  9046  canthp1lem2  9048  pwfseqlem4a  9056  pwfseqlem4  9057  ltbwe  18264  vitali  22148  fin2so  30245  weeq12d  31189  dnwech  31198  aomclem5  31208  aomclem6  31209  aomclem7  31210