Theorem preq12d 4685

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  opeq1  4816  csbopg  4834  opthhausdorff  5471  opthhausdorff0  5472  f1oprswap  6825  wunex2  10661  wuncval2  10670  s4prop  14872  wrdlen2  14906  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  wrd2f1tovbij  14922  prdsval  17418  xpsfval  17530  xpsval  17534  ipoval  18496  frmdval  18819  symg2bas  19368  xpstopnlem2  23776  tusval  24230  tmsval  24446  tmsxpsval  24503  uniiccdif  25545  dchrval  27197  eengv  29048  wkslem1  29676  wkslem2  29677  iswlk  29679  wlkonl1iedg  29732  2wlklem  29734  redwlk  29739  wlkp1lem7  29746  wlkdlem2  29750  upgrwlkdvdelem  29804  usgr2pthlem  29831  usgr2pth  29832  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  iswwlks  29904  0enwwlksnge1  29932  wlkiswwlks2lem2  29938  wlkiswwlks2lem5  29941  wwlksm1edg  29949  wwlksnred  29960  wwlksnext  29961  wwlksnredwwlkn  29963  wwlksnextproplem2  29978  2wlkdlem10  30003  usgrwwlks2on  30026  umgrwwlks2on  30027  rusgrnumwwlkl1  30039  isclwwlk  30054  clwwlkccatlem  30059  clwwlkccat  30060  clwlkclwwlklem2a1  30062  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlk  30072  clwwisshclwwslemlem  30083  clwwisshclwwslem  30084  clwwisshclwws  30085  clwwlkinwwlk  30110  clwwlkn2  30114  clwwlkel  30116  clwwlkf  30117  clwwlkwwlksb  30124  clwwlkext2edg  30126  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  umgr2cwwk2dif  30134  s2elclwwlknon2  30174  clwwlknonex2lem2  30178  clwwlknonex2  30179  3wlkdlem10  30239  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupthseg  30276  upgreupthseg  30279  eupth2lem3  30306  nfrgr2v  30342  frgr3vlem1  30343  frgr3vlem2  30344  4cycl2vnunb  30360  disjdifprg  32645  s2rnOLD  33004  idlsrgval  33563  revwlk  35307  kur14lem1  35388  kur14  35398  bj-endval  37629  tgrpfset  41190  tgrpset  41191  hlhilset  42380  dfac21  43494  mendval  43607  oaun2  43809  mnurndlem1  44708  sge0sn  46807  isuspgrimlem  48371  upgrimwlklem5  48377  grtriproplem  48415  isgrtri  48419  grtriclwlk3  48421  cycl3grtrilem  48422  stgrfv  48429  gpgov  48518  gpgprismgriedgdmss  48528  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgedgiov  48541  gpg3kgrtriexlem6  48564  gpg3kgrtriex  48565  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem10  48580  pgnbgreunbgr  48601  gpg5edgnedg  48606  grlimedgnedg  48607  isupwlk  48612  zlmodzxzsub  48836  2arymaptf  49128  prelrrx2b  49190  rrx2plordisom  49199  onsetreclem1  50180