Theorem weeq2 5612

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 5592	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
2		soeq2 5554	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)))
4		df-we 5579	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5579	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   Or wor 5531   Fr wfr 5574   We wwe 5576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ral 3052  df-ss 3918  df-po 5532  df-so 5533  df-fr 5577  df-we 5579

This theorem is referenced by:  weeq12d  5613  ordeq  6324  0we1  8433  oieq2  9418  wemapwe  9606  ween  9945  dfac8  10046  weth  10405  pwfseqlem4a  10572  pwfseqlem4  10573  ltweuz  13884  ltwenn  13885  bpolylem  15971  ltbwe  21999  vitali  25570  aomclem6  43301  omeiunle  46761