Theorem weeq2 5651

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
weeq2	⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵))

Proof of Theorem weeq2

Step	Hyp	Ref	Expression
1		freq2 5631	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
2		soeq2 5593	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)))
4		df-we 5618	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5618	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   Or wor 5570   Fr wfr 5613   We wwe 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ral 3080  df-ss 3923  df-po 5571  df-so 5572  df-fr 5616  df-we 5618

This theorem is referenced by:  weeq12d  5652  ordeq  6369  0we1  8492  oieq2  9476  wemapwe  9667  ween  10020  dfac8  10120  weth  10480  pwfseqlem4a  10647  pwfseqlem4  10648  ltweuz  13999  ltwenn  14000  bpolylem  16103  ltbwe  22176  vitali  25753  aomclem6  43769  omeiunle  47214