Theorem weeq1 4713

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 4695	. . 3 |- ( R = S -> ( R Fr A <-> S Fr A ) )
2		soeq1 4665	. . 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 4686	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
5		df-we 4686	. 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 1369   Or wor 4645   Fr wfr 4681   We wwe 4683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-ral 2725  df-rex 2726  df-br 4298  df-po 4646  df-so 4647  df-fr 4684  df-we 4686

This theorem is referenced by:  oieq1  7731  hartogslem1  7761  wemapwe  7933  wemapweOLD  7934  infxpenlem  8185  dfac8b  8206  ac10ct  8209  fpwwe2cbv  8802  fpwwe2lem2  8804  fpwwe2lem5  8806  fpwwecbv  8816  fpwwelem  8817  canthnumlem  8820  canthwelem  8822  canthwe  8823  canthp1lem2  8825  pwfseqlem4a  8833  pwfseqlem4  8834  ltbwe  17559  vitali  21098  fin2so  28421  weeq12d  29397  dnwech  29406  aomclem5  29416  aomclem6  29417  aomclem7  29418