Theorem weeq2 5643

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 5623	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
2		soeq2 5585	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)))
4		df-we 5610	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5610	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   Or wor 5562   Fr wfr 5605   We wwe 5607

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ral 3077  df-ss 3916  df-po 5563  df-so 5564  df-fr 5608  df-we 5610

This theorem is used by:  weeq12d  5644  ordeq  6364  0we1  8493  oieq2  9485  wemapwe  9676  ween  10038  dfac8  10138  weth  10497  pwfseqlem4a  10670  pwfseqlem4  10671  ltweuz  14025  ltwenn  14026  bpolylem  16134  ltbwe  22260  vitali  25841  aomclem6  43900  omeiunle  47345