Theorem weeq2 5646

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 5626	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
2		soeq2 5588	. . 3 ⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)))
4		df-we 5613	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
5		df-we 5613	. 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 5565   Fr wfr 5608   We wwe 5610

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ral 3081  df-ss 3901  df-po 5566  df-so 5567  df-fr 5611  df-we 5613

This theorem is used by:  weeq12d  5647  ordeq  6395  0we1  8552  oieq2  9544  wemapwe  9735  ween  10153  dfac8  10253  weth  10612  pwfseqlem4a  10785  pwfseqlem4  10786  ltweuz  14144  ltwenn  14145  bpolylem  16258  ltbwe  22408  vitali  25989  ltwenn0  33635  acwer1prclem  35892  onprcf1acwevdlem1  36086  aomclem6  44327  omeiunle  47800