Theorem preq12d 4700

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

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

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 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  opeq1  4831  csbopg  4849  opthhausdorff  5473  opthhausdorff0  5474  f1oprswap  6827  wunex2  10661  wuncval2  10670  s4prop  14845  wrdlen2  14879  wwlktovf  14891  wwlktovf1  14892  wwlktovfo  14893  wrd2f1tovbij  14895  prdsval  17387  xpsfval  17499  xpsval  17503  ipoval  18465  frmdval  18788  symg2bas  19334  xpstopnlem2  23767  tusval  24221  tmsval  24437  tmsxpsval  24494  uniiccdif  25547  dchrval  27213  eengv  29064  wkslem1  29693  wkslem2  29694  iswlk  29696  wlkonl1iedg  29749  2wlklem  29751  redwlk  29756  wlkp1lem7  29763  wlkdlem2  29767  upgrwlkdvdelem  29821  usgr2pthlem  29848  usgr2pth  29849  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  iswwlks  29921  0enwwlksnge1  29949  wlkiswwlks2lem2  29955  wlkiswwlks2lem5  29958  wwlksm1edg  29966  wwlksnred  29977  wwlksnext  29978  wwlksnredwwlkn  29980  wwlksnextproplem2  29995  2wlkdlem10  30020  usgrwwlks2on  30043  umgrwwlks2on  30044  rusgrnumwwlkl1  30056  isclwwlk  30071  clwwlkccatlem  30076  clwwlkccat  30077  clwlkclwwlklem2a1  30079  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlk  30089  clwwisshclwwslemlem  30100  clwwisshclwwslem  30101  clwwisshclwws  30102  clwwlkinwwlk  30127  clwwlkn2  30131  clwwlkel  30133  clwwlkf  30134  clwwlkwwlksb  30141  clwwlkext2edg  30143  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  umgr2cwwk2dif  30151  s2elclwwlknon2  30191  clwwlknonex2lem2  30195  clwwlknonex2  30196  3wlkdlem10  30256  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eupthseg  30293  upgreupthseg  30296  eupth2lem3  30323  nfrgr2v  30359  frgr3vlem1  30360  frgr3vlem2  30361  4cycl2vnunb  30377  disjdifprg  32661  s2rnOLD  33036  idlsrgval  33595  revwlk  35338  kur14lem1  35419  kur14  35429  bj-endval  37564  tgrpfset  41114  tgrpset  41115  hlhilset  42304  dfac21  43417  mendval  43530  oaun2  43732  mnurndlem1  44631  sge0sn  46731  isuspgrimlem  48249  upgrimwlklem5  48255  grtriproplem  48293  isgrtri  48297  grtriclwlk3  48299  cycl3grtrilem  48300  stgrfv  48307  gpgov  48396  gpgprismgriedgdmss  48406  gpgedgvtx0  48415  gpgedgvtx1  48416  gpgedgiov  48419  gpg3kgrtriexlem6  48442  gpg3kgrtriex  48443  gpgprismgr4cycllem3  48451  gpgprismgr4cycllem10  48458  pgnbgreunbgr  48479  gpg5edgnedg  48484  grlimedgnedg  48485  isupwlk  48490  zlmodzxzsub  48714  2arymaptf  49006  prelrrx2b  49068  rrx2plordisom  49077  onsetreclem1  50058