Theorem preq12d 4692

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

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

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-un 3905  df-sn 4575  df-pr 4577

This theorem is referenced by:  opeq1  4823  csbopg  4841  opthhausdorff  5455  opthhausdorff0  5456  f1oprswap  6803  wunex2  10621  wuncval2  10630  s4prop  14809  wrdlen2  14843  wwlktovf  14855  wwlktovf1  14856  wwlktovfo  14857  wrd2f1tovbij  14859  prdsval  17351  xpsfval  17462  xpsval  17466  ipoval  18428  frmdval  18751  symg2bas  19298  xpstopnlem2  23719  tusval  24173  tmsval  24389  tmsxpsval  24446  uniiccdif  25499  dchrval  27165  eengv  28950  wkslem1  29579  wkslem2  29580  iswlk  29582  wlkonl1iedg  29635  2wlklem  29637  redwlk  29642  wlkp1lem7  29649  wlkdlem2  29653  upgrwlkdvdelem  29707  usgr2pthlem  29734  usgr2pth  29735  crctcshwlkn0lem4  29784  crctcshwlkn0lem5  29785  crctcshwlkn0lem6  29786  iswwlks  29807  0enwwlksnge1  29835  wlkiswwlks2lem2  29841  wlkiswwlks2lem5  29844  wwlksm1edg  29852  wwlksnred  29863  wwlksnext  29864  wwlksnredwwlkn  29866  wwlksnextproplem2  29881  2wlkdlem10  29906  umgrwwlks2on  29928  rusgrnumwwlkl1  29939  isclwwlk  29954  clwwlkccatlem  29959  clwwlkccat  29960  clwlkclwwlklem2a1  29962  clwlkclwwlklem2fv1  29965  clwlkclwwlklem2a4  29967  clwlkclwwlklem2a  29968  clwlkclwwlklem2  29970  clwlkclwwlk  29972  clwwisshclwwslemlem  29983  clwwisshclwwslem  29984  clwwisshclwws  29985  clwwlkinwwlk  30010  clwwlkn2  30014  clwwlkel  30016  clwwlkf  30017  clwwlkwwlksb  30024  clwwlkext2edg  30026  wwlksext2clwwlk  30027  wwlksubclwwlk  30028  umgr2cwwk2dif  30034  s2elclwwlknon2  30074  clwwlknonex2lem2  30078  clwwlknonex2  30079  3wlkdlem10  30139  upgr3v3e3cycl  30150  upgr4cycl4dv4e  30155  eupthseg  30176  upgreupthseg  30179  eupth2lem3  30206  nfrgr2v  30242  frgr3vlem1  30243  frgr3vlem2  30244  4cycl2vnunb  30260  disjdifprg  32545  s2rnOLD  32915  idlsrgval  33458  revwlk  35137  kur14lem1  35218  kur14  35228  bj-endval  37328  tgrpfset  40762  tgrpset  40763  hlhilset  41952  dfac21  43078  mendval  43191  oaun2  43393  mnurndlem1  44293  sge0sn  46396  isuspgrimlem  47905  upgrimwlklem5  47911  grtriproplem  47949  isgrtri  47953  grtriclwlk3  47955  cycl3grtrilem  47956  stgrfv  47963  gpgov  48052  gpgprismgriedgdmss  48062  gpgedgvtx0  48071  gpgedgvtx1  48072  gpgedgiov  48075  gpg3kgrtriexlem6  48098  gpg3kgrtriex  48099  gpgprismgr4cycllem3  48107  gpgprismgr4cycllem10  48114  pgnbgreunbgr  48135  gpg5edgnedg  48140  grlimedgnedg  48141  isupwlk  48146  zlmodzxzsub  48370  2arymaptf  48663  prelrrx2b  48725  rrx2plordisom  48734  onsetreclem1  49716