MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  weeq2 Structured version   Visualization version   GIF version

Theorem weeq2 5677
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
weeq2 (𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))

Proof of Theorem weeq2
StepHypRef Expression
1 freq2 5657 . . 3 (𝐴 = 𝐵 → (𝑅 Fr 𝐴𝑅 Fr 𝐵))
2 soeq2 5619 . . 3 (𝐴 = 𝐵 → (𝑅 Or 𝐴𝑅 Or 𝐵))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵)))
4 df-we 5643 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
5 df-we 5643 . 2 (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵𝑅 Or 𝐵))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537   Or wor 5596   Fr wfr 5638   We wwe 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ral 3060  df-ss 3980  df-po 5597  df-so 5598  df-fr 5641  df-we 5643
This theorem is referenced by:  weeq12d  5678  ordeq  6393  0we1  8543  oieq2  9551  wemapwe  9735  ween  10073  dfac8  10174  weth  10533  pwfseqlem4a  10699  pwfseqlem4  10700  ltweuz  13999  ltwenn  14000  bpolylem  16081  ltbwe  22080  vitali  25662  aomclem6  43048  omeiunle  46473
  Copyright terms: Public domain W3C validator