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

Theorem preq12bg 4747
 Description: Closed form of preq12b 4744. (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 4632 . . . . . . 7 (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
21eqeq1d 2803 . . . . . 6 (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
3 eqeq1 2805 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 = 𝑧𝐴 = 𝑧))
43anbi1d 632 . . . . . . 7 (𝑥 = 𝐴 → ((𝑥 = 𝑧𝑦 = 𝐷) ↔ (𝐴 = 𝑧𝑦 = 𝐷)))
5 eqeq1 2805 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 = 𝐷𝐴 = 𝐷))
65anbi1d 632 . . . . . . 7 (𝑥 = 𝐴 → ((𝑥 = 𝐷𝑦 = 𝑧) ↔ (𝐴 = 𝐷𝑦 = 𝑧)))
74, 6orbi12d 916 . . . . . 6 (𝑥 = 𝐴 → (((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧))))
82, 7bibi12d 349 . . . . 5 (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧)))))
98imbi2d 344 . . . 4 (𝑥 = 𝐴 → ((𝐷𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧)))) ↔ (𝐷𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧))))))
10 preq2 4633 . . . . . . 7 (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
1110eqeq1d 2803 . . . . . 6 (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
12 eqeq1 2805 . . . . . . . 8 (𝑦 = 𝐵 → (𝑦 = 𝐷𝐵 = 𝐷))
1312anbi2d 631 . . . . . . 7 (𝑦 = 𝐵 → ((𝐴 = 𝑧𝑦 = 𝐷) ↔ (𝐴 = 𝑧𝐵 = 𝐷)))
14 eqeq1 2805 . . . . . . . 8 (𝑦 = 𝐵 → (𝑦 = 𝑧𝐵 = 𝑧))
1514anbi2d 631 . . . . . . 7 (𝑦 = 𝐵 → ((𝐴 = 𝐷𝑦 = 𝑧) ↔ (𝐴 = 𝐷𝐵 = 𝑧)))
1613, 15orbi12d 916 . . . . . 6 (𝑦 = 𝐵 → (((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧))))
1711, 16bibi12d 349 . . . . 5 (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧)))))
1817imbi2d 344 . . . 4 (𝑦 = 𝐵 → ((𝐷𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝑦 = 𝐷) ∨ (𝐴 = 𝐷𝑦 = 𝑧)))) ↔ (𝐷𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧))))))
19 preq1 4632 . . . . . . 7 (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
2019eqeq2d 2812 . . . . . 6 (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21 eqeq2 2813 . . . . . . . 8 (𝑧 = 𝐶 → (𝐴 = 𝑧𝐴 = 𝐶))
2221anbi1d 632 . . . . . . 7 (𝑧 = 𝐶 → ((𝐴 = 𝑧𝐵 = 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
23 eqeq2 2813 . . . . . . . 8 (𝑧 = 𝐶 → (𝐵 = 𝑧𝐵 = 𝐶))
2423anbi2d 631 . . . . . . 7 (𝑧 = 𝐶 → ((𝐴 = 𝐷𝐵 = 𝑧) ↔ (𝐴 = 𝐷𝐵 = 𝐶)))
2522, 24orbi12d 916 . . . . . 6 (𝑧 = 𝐶 → (((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))
2620, 25bibi12d 349 . . . . 5 (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶)))))
2726imbi2d 344 . . . 4 (𝑧 = 𝐶 → ((𝐷𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝑧)))) ↔ (𝐷𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))))
28 preq2 4633 . . . . . . 7 (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
2928eqeq2d 2812 . . . . . 6 (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
30 eqeq2 2813 . . . . . . . 8 (𝑤 = 𝐷 → (𝑦 = 𝑤𝑦 = 𝐷))
3130anbi2d 631 . . . . . . 7 (𝑤 = 𝐷 → ((𝑥 = 𝑧𝑦 = 𝑤) ↔ (𝑥 = 𝑧𝑦 = 𝐷)))
32 eqeq2 2813 . . . . . . . 8 (𝑤 = 𝐷 → (𝑥 = 𝑤𝑥 = 𝐷))
3332anbi1d 632 . . . . . . 7 (𝑤 = 𝐷 → ((𝑥 = 𝑤𝑦 = 𝑧) ↔ (𝑥 = 𝐷𝑦 = 𝑧)))
3431, 33orbi12d 916 . . . . . 6 (𝑤 = 𝐷 → (((𝑥 = 𝑧𝑦 = 𝑤) ∨ (𝑥 = 𝑤𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧))))
35 vex 3447 . . . . . . 7 𝑥 ∈ V
36 vex 3447 . . . . . . 7 𝑦 ∈ V
37 vex 3447 . . . . . . 7 𝑧 ∈ V
38 vex 3447 . . . . . . 7 𝑤 ∈ V
3935, 36, 37, 38preq12b 4744 . . . . . 6 ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧𝑦 = 𝑤) ∨ (𝑥 = 𝑤𝑦 = 𝑧)))
4029, 34, 39vtoclbg 3520 . . . . 5 (𝐷𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧))))
4140a1i 11 . . . 4 ((𝑥𝑉𝑦𝑊𝑧𝑋) → (𝐷𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧𝑦 = 𝐷) ∨ (𝑥 = 𝐷𝑦 = 𝑧)))))
429, 18, 27, 41vtocl3ga 3529 . . 3 ((𝐴𝑉𝐵𝑊𝐶𝑋) → (𝐷𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶)))))
43423expa 1115 . 2 (((𝐴𝑉𝐵𝑊) ∧ 𝐶𝑋) → (𝐷𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶)))))
4443impr 458 1 (((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶𝐵 = 𝐷) ∨ (𝐴 = 𝐷𝐵 = 𝐶))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  {cpr 4530 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531 This theorem is referenced by:  prneimg  4748  pr1eqbg  4750  preqsnd  4752  preq12nebg  4756  opthprneg  4758  preleqALT  9068  pythagtriplem2  16147  pythagtrip  16164  upgrpredgv  26935  uhgr2edg  27001  usgredg2v  27020  2pthon3v  27732  opprb  43610  or2expropbi  43613  ich2exprop  43975  prsprel  43991  paireqne  44015  poprelb  44028
 Copyright terms: Public domain W3C validator