Theorem preq12d 4678

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 4672	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → {𝐴, 𝐶} = {𝐵, 𝐷})
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})

Syntax hints:   → wi 4   = wceq 1539  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-pr 4565

This theorem is referenced by:  opeq1  4805  csbopg  4823  opthhausdorff  5432  opthhausdorff0  5433  f1oprswap  6769  wunex2  10503  wuncval2  10512  s4prop  14632  wrdlen2  14666  wwlktovf  14680  wwlktovf1  14681  wwlktovfo  14682  wrd2f1tovbij  14684  prdsval  17175  xpsfval  17286  xpsval  17290  ipoval  18257  frmdval  18499  symg2bas  19009  xpstopnlem2  22971  tusval  23426  tmsval  23645  tmsxpsval  23703  uniiccdif  24751  dchrval  26391  eengv  27356  wkslem1  27983  wkslem2  27984  iswlk  27986  wlkonl1iedg  28042  2wlklem  28044  redwlk  28049  wlkp1lem7  28056  wlkdlem2  28060  upgrwlkdvdelem  28113  usgr2pthlem  28140  usgr2pth  28141  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem6  28189  iswwlks  28210  0enwwlksnge1  28238  wlkiswwlks2lem2  28244  wlkiswwlks2lem5  28247  wwlksm1edg  28255  wwlksnred  28266  wwlksnext  28267  wwlksnredwwlkn  28269  wwlksnextproplem2  28284  2wlkdlem10  28309  umgrwwlks2on  28331  rusgrnumwwlkl1  28342  isclwwlk  28357  clwwlkccatlem  28362  clwwlkccat  28363  clwlkclwwlklem2a1  28365  clwlkclwwlklem2fv1  28368  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwlkclwwlk  28375  clwwisshclwwslemlem  28386  clwwisshclwwslem  28387  clwwisshclwws  28388  clwwlkinwwlk  28413  clwwlkn2  28417  clwwlkel  28419  clwwlkf  28420  clwwlkwwlksb  28427  clwwlkext2edg  28429  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  umgr2cwwk2dif  28437  s2elclwwlknon2  28477  clwwlknonex2lem2  28481  clwwlknonex2  28482  3wlkdlem10  28542  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  eupthseg  28579  upgreupthseg  28582  eupth2lem3  28609  nfrgr2v  28645  frgr3vlem1  28646  frgr3vlem2  28647  4cycl2vnunb  28663  disjdifprg  30923  s2rn  31227  idlsrgval  31657  revwlk  33095  kur14lem1  33177  kur14  33187  bj-endval  35495  tgrpfset  38765  tgrpset  38766  hlhilset  39955  dfac21  40898  mendval  41015  mnurndlem1  41906  sge0sn  43924  isomuspgrlem2b  45292  isupwlk  45309  zlmodzxzsub  45707  2arymaptf  46009  prelrrx2b  46071  rrx2plordisom  46080  onsetreclem1  46421