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

Theorem preq12bg 4853
Description: Closed form of preq12b 4850. (Contributed by Scott Fenton, 28-Mar-2014.)
Assertion
Ref Expression
preq12bg (((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))

Proof of Theorem preq12bg
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq1 4733 . . . . . . 7 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21eqeq1d 2739 . . . . . 6 (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
3 eqeq1 2741 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 = 𝑧𝐴 = 𝑧))
43anbi1d 631 . . . . . . 7 (𝑥 = 𝐴 → ((𝑥 = 𝑧𝑦 = 𝐷) ↔ (𝐴 = 𝑧𝑦 = 𝐷)))
5 eqeq1 2741 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 = 𝐷𝐴 = 𝐷))
65anbi1d 631 . . . . . . 7 (𝑥 = 𝐴 → ((𝑥 = 𝐷𝑦 = 𝑧) ↔ (𝐴 = 𝐷𝑦 = 𝑧)))
74, 6orbi12d 919 . . . . . 6 (𝑥 = 𝐴 → (((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧))))
82, 7bibi12d 345 . . . . 5 (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧)))))
98imbi2d 340 . . . 4 (𝑥 = 𝐴 → ((𝐷𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧)))) ↔ (𝐷𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧))))))
10 preq2 4734 . . . . . . 7 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
1110eqeq1d 2739 . . . . . 6 (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
12 eqeq1 2741 . . . . . . . 8 (𝑦 = 𝐵 → (𝑦 = 𝐷𝐵 = 𝐷))
1312anbi2d 630 . . . . . . 7 (𝑦 = 𝐵 → ((𝐴 = 𝑧𝑦 = 𝐷) ↔ (𝐴 = 𝑧𝐵 = 𝐷)))
14 eqeq1 2741 . . . . . . . 8 (𝑦 = 𝐵 → (𝑦 = 𝑧𝐵 = 𝑧))
1514anbi2d 630 . . . . . . 7 (𝑦 = 𝐵 → ((𝐴 = 𝐷𝑦 = 𝑧) ↔ (𝐴 = 𝐷𝐵 = 𝑧)))
1613, 15orbi12d 919 . . . . . 6 (𝑦 = 𝐵 → (((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧))))
1711, 16bibi12d 345 . . . . 5 (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧)))))
1817imbi2d 340 . . . 4 (𝑦 = 𝐵 → ((𝐷𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧)))) ↔ (𝐷𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧))))))
19 preq1 4733 . . . . . . 7 (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
2019eqeq2d 2748 . . . . . 6 (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21 eqeq2 2749 . . . . . . . 8 (𝑧 = 𝐶 → (𝐴 = 𝑧𝐴 = 𝐶))
2221anbi1d 631 . . . . . . 7 (𝑧 = 𝐶 → ((𝐴 = 𝑧𝐵 = 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
23 eqeq2 2749 . . . . . . . 8 (𝑧 = 𝐶 → (𝐵 = 𝑧𝐵 = 𝐶))
2423anbi2d 630 . . . . . . 7 (𝑧 = 𝐶 → ((𝐴 = 𝐷𝐵 = 𝑧) ↔ (𝐴 = 𝐷𝐵 = 𝐶)))
2522, 24orbi12d 919 . . . . . 6 (𝑧 = 𝐶 → (((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))
2620, 25bibi12d 345 . . . . 5 (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶)))))
2726imbi2d 340 . . . 4 (𝑧 = 𝐶 → ((𝐷𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧)))) ↔ (𝐷𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))))
28 preq2 4734 . . . . . . 7 (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
2928eqeq2d 2748 . . . . . 6 (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
30 eqeq2 2749 . . . . . . . 8 (𝑤 = 𝐷 → (𝑦 = 𝑤𝑦 = 𝐷))
3130anbi2d 630 . . . . . . 7 (𝑤 = 𝐷 → ((𝑥 = 𝑧𝑦 = 𝑤) ↔ (𝑥 = 𝑧𝑦 = 𝐷)))
32 eqeq2 2749 . . . . . . . 8 (𝑤 = 𝐷 → (𝑥 = 𝑤𝑥 = 𝐷))
3332anbi1d 631 . . . . . . 7 (𝑤 = 𝐷 → ((𝑥 = 𝑤𝑦 = 𝑧) ↔ (𝑥 = 𝐷𝑦 = 𝑧)))
3431, 33orbi12d 919 . . . . . 6 (𝑤 = 𝐷 → (((𝑥 = 𝑧𝑦 = 𝑤) ∨ (𝑥 = 𝑤𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧))))
35 vex 3484 . . . . . . 7 𝑥 ∈ V
36 vex 3484 . . . . . . 7 𝑦 ∈ V
37 vex 3484 . . . . . . 7 𝑧 ∈ V
38 vex 3484 . . . . . . 7 𝑤 ∈ V
3935, 36, 37, 38preq12b 4850 . . . . . 6 ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧𝑦 = 𝑤) ∨ (𝑥 = 𝑤𝑦 = 𝑧)))
4029, 34, 39vtoclbg 3557 . . . . 5 (𝐷𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧))))
4140a1i 11 . . . 4 ((𝑥𝑉𝑦𝑊𝑧𝑋) → (𝐷𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧)))))
429, 18, 27, 41vtocl3ga 3583 . . 3 ((𝐴𝑉𝐵𝑊𝐶𝑋) → (𝐷𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶)))))
43423expa 1119 . 2 (((𝐴𝑉𝐵𝑊) ∧ 𝐶𝑋) → (𝐷𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶)))))
4443impr 454 1 (((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  {cpr 4628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629
This theorem is referenced by:  prneimg  4854  prneimg2  4855  pr1eqbg  4857  preqsnd  4859  preq12nebg  4863  opthprneg  4865  preleqALT  9657  pythagtriplem2  16855  pythagtrip  16872  upgrpredgv  29156  uhgr2edg  29225  usgredg2v  29244  2pthon3v  29963  opprb  47043  or2expropbi  47046  ich2exprop  47458  prsprel  47474  paireqne  47498  poprelb  47511  gpgvtxedg0  48021  gpgvtxedg1  48022
  Copyright terms: Public domain W3C validator