Theorem preq12d 4693

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4577

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4576  df-pr 4578

This theorem is referenced by:  opeq1  4824  csbopg  4842  opthhausdorff  5460  opthhausdorff0  5461  f1oprswap  6813  wunex2  10636  wuncval2  10645  s4prop  14819  wrdlen2  14853  wwlktovf  14865  wwlktovf1  14866  wwlktovfo  14867  wrd2f1tovbij  14869  prdsval  17361  xpsfval  17472  xpsval  17476  ipoval  18438  frmdval  18761  symg2bas  19307  xpstopnlem2  23727  tusval  24181  tmsval  24397  tmsxpsval  24454  uniiccdif  25507  dchrval  27173  eengv  28959  wkslem1  29588  wkslem2  29589  iswlk  29591  wlkonl1iedg  29644  2wlklem  29646  redwlk  29651  wlkp1lem7  29658  wlkdlem2  29662  upgrwlkdvdelem  29716  usgr2pthlem  29743  usgr2pth  29744  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0lem6  29795  iswwlks  29816  0enwwlksnge1  29844  wlkiswwlks2lem2  29850  wlkiswwlks2lem5  29853  wwlksm1edg  29861  wwlksnred  29872  wwlksnext  29873  wwlksnredwwlkn  29875  wwlksnextproplem2  29890  2wlkdlem10  29915  usgrwwlks2on  29938  umgrwwlks2on  29939  rusgrnumwwlkl1  29951  isclwwlk  29966  clwwlkccatlem  29971  clwwlkccat  29972  clwlkclwwlklem2a1  29974  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwlkclwwlk  29984  clwwisshclwwslemlem  29995  clwwisshclwwslem  29996  clwwisshclwws  29997  clwwlkinwwlk  30022  clwwlkn2  30026  clwwlkel  30028  clwwlkf  30029  clwwlkwwlksb  30036  clwwlkext2edg  30038  wwlksext2clwwlk  30039  wwlksubclwwlk  30040  umgr2cwwk2dif  30046  s2elclwwlknon2  30086  clwwlknonex2lem2  30090  clwwlknonex2  30091  3wlkdlem10  30151  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  eupthseg  30188  upgreupthseg  30191  eupth2lem3  30218  nfrgr2v  30254  frgr3vlem1  30255  frgr3vlem2  30256  4cycl2vnunb  30272  disjdifprg  32557  s2rnOLD  32932  idlsrgval  33475  revwlk  35190  kur14lem1  35271  kur14  35281  bj-endval  37380  tgrpfset  40863  tgrpset  40864  hlhilset  42053  dfac21  43183  mendval  43296  oaun2  43498  mnurndlem1  44398  sge0sn  46501  isuspgrimlem  48019  upgrimwlklem5  48025  grtriproplem  48063  isgrtri  48067  grtriclwlk3  48069  cycl3grtrilem  48070  stgrfv  48077  gpgov  48166  gpgprismgriedgdmss  48176  gpgedgvtx0  48185  gpgedgvtx1  48186  gpgedgiov  48189  gpg3kgrtriexlem6  48212  gpg3kgrtriex  48213  gpgprismgr4cycllem3  48221  gpgprismgr4cycllem10  48228  pgnbgreunbgr  48249  gpg5edgnedg  48254  grlimedgnedg  48255  isupwlk  48260  zlmodzxzsub  48484  2arymaptf  48777  prelrrx2b  48839  rrx2plordisom  48848  onsetreclem1  49830