Theorem preq12d 4686

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

Syntax hints:   → wi 4   = wceq 1542  {cpr 4570

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  opeq1  4817  csbopg  4835  opthhausdorff  5465  opthhausdorff0  5466  f1oprswap  6819  wunex2  10652  wuncval2  10661  s4prop  14863  wrdlen2  14897  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  wrd2f1tovbij  14913  prdsval  17409  xpsfval  17521  xpsval  17525  ipoval  18487  frmdval  18810  symg2bas  19359  xpstopnlem2  23786  tusval  24240  tmsval  24456  tmsxpsval  24513  uniiccdif  25555  dchrval  27211  eengv  29062  wkslem1  29691  wkslem2  29692  iswlk  29694  wlkonl1iedg  29747  2wlklem  29749  redwlk  29754  wlkp1lem7  29761  wlkdlem2  29765  upgrwlkdvdelem  29819  usgr2pthlem  29846  usgr2pth  29847  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0lem6  29898  iswwlks  29919  0enwwlksnge1  29947  wlkiswwlks2lem2  29953  wlkiswwlks2lem5  29956  wwlksm1edg  29964  wwlksnred  29975  wwlksnext  29976  wwlksnredwwlkn  29978  wwlksnextproplem2  29993  2wlkdlem10  30018  usgrwwlks2on  30041  umgrwwlks2on  30042  rusgrnumwwlkl1  30054  isclwwlk  30069  clwwlkccatlem  30074  clwwlkccat  30075  clwlkclwwlklem2a1  30077  clwlkclwwlklem2fv1  30080  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwlkclwwlk  30087  clwwisshclwwslemlem  30098  clwwisshclwwslem  30099  clwwisshclwws  30100  clwwlkinwwlk  30125  clwwlkn2  30129  clwwlkel  30131  clwwlkf  30132  clwwlkwwlksb  30139  clwwlkext2edg  30141  wwlksext2clwwlk  30142  wwlksubclwwlk  30143  umgr2cwwk2dif  30149  s2elclwwlknon2  30189  clwwlknonex2lem2  30193  clwwlknonex2  30194  3wlkdlem10  30254  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eupthseg  30291  upgreupthseg  30294  eupth2lem3  30321  nfrgr2v  30357  frgr3vlem1  30358  frgr3vlem2  30359  4cycl2vnunb  30375  disjdifprg  32660  s2rnOLD  33019  idlsrgval  33578  revwlk  35323  kur14lem1  35404  kur14  35414  bj-endval  37645  tgrpfset  41204  tgrpset  41205  hlhilset  42394  dfac21  43512  mendval  43625  oaun2  43827  mnurndlem1  44726  sge0sn  46825  isuspgrimlem  48383  upgrimwlklem5  48389  grtriproplem  48427  isgrtri  48431  grtriclwlk3  48433  cycl3grtrilem  48434  stgrfv  48441  gpgov  48530  gpgprismgriedgdmss  48540  gpgedgvtx0  48549  gpgedgvtx1  48550  gpgedgiov  48553  gpg3kgrtriexlem6  48576  gpg3kgrtriex  48577  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem10  48592  pgnbgreunbgr  48613  gpg5edgnedg  48618  grlimedgnedg  48619  isupwlk  48624  zlmodzxzsub  48848  2arymaptf  49140  prelrrx2b  49202  rrx2plordisom  49211  onsetreclem1  50192