Theorem preq12d 4677

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypotheses

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
preq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
preq12d	⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Proof of Theorem preq12d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		preq12 4671	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
4	1, 2, 3	syl2anc 586	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Syntax hints:   → wi 4   = wceq 1537  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  opeq1  4803  csbopg  4821  opthhausdorff  5407  opthhausdorff0  5408  f1oprswap  6658  wunex2  10160  wuncval2  10169  s4prop  14272  wrdlen2  14306  wwlktovf  14320  wwlktovf1  14321  wwlktovfo  14322  wrd2f1tovbij  14324  prdsval  16728  xpsfval  16839  xpsval  16843  ipoval  17764  frmdval  18016  symg2bas  18521  xpstopnlem2  22419  tusval  22875  tmsval  23091  tmsxpsval  23148  uniiccdif  24179  dchrval  25810  eengv  26765  wkslem1  27389  wkslem2  27390  iswlk  27392  wlkonl1iedg  27447  2wlklem  27449  redwlk  27454  wlkp1lem7  27461  wlkdlem2  27465  upgrwlkdvdelem  27517  usgr2pthlem  27544  usgr2pth  27545  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  iswwlks  27614  0enwwlksnge1  27642  wlkiswwlks2lem2  27648  wlkiswwlks2lem5  27651  wwlksm1edg  27659  wwlksnred  27670  wwlksnext  27671  wwlksnredwwlkn  27673  wwlksnextproplem2  27689  2wlkdlem10  27714  umgrwwlks2on  27736  rusgrnumwwlkl1  27747  isclwwlk  27762  clwwlkccatlem  27767  clwwlkccat  27768  clwlkclwwlklem2a1  27770  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlk  27780  clwwisshclwwslemlem  27791  clwwisshclwwslem  27792  clwwisshclwws  27793  clwwlkinwwlk  27818  clwwlkn2  27822  clwwlkel  27825  clwwlkf  27826  clwwlkwwlksb  27833  clwwlkext2edg  27835  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  umgr2cwwk2dif  27843  s2elclwwlknon2  27883  clwwlknonex2lem2  27887  clwwlknonex2  27888  3wlkdlem10  27948  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupthseg  27985  upgreupthseg  27988  eupth2lem3  28015  nfrgr2v  28051  frgr3vlem1  28052  frgr3vlem2  28053  4cycl2vnunb  28069  disjdifprg  30325  s2rn  30620  revwlk  32371  kur14lem1  32453  kur14  32463  bj-endval  34599  tgrpfset  37895  tgrpset  37896  hlhilset  39085  dfac21  39686  mendval  39803  mnurndlem1  40637  sge0sn  42681  isomuspgrlem2b  44014  isupwlk  44031  zlmodzxzsub  44428  prelrrx2b  44721  rrx2plordisom  44730  onsetreclem1  44827