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 633	. 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 1542   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-ss 3907  df-po 5532  df-so 5533  df-fr 5577  df-we 5579

This theorem is referenced by:  weeq12d  5613  ordeq  6324  0we1  8434  oieq2  9421  wemapwe  9609  ween  9948  dfac8  10049  weth  10408  pwfseqlem4a  10575  pwfseqlem4  10576  ltweuz  13914  ltwenn  13915  bpolylem  16004  ltbwe  22032  vitali  25590  aomclem6  43505  omeiunle  46963