Theorem preq12d 4708

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  opeq1  4840  csbopg  4858  opthhausdorff  5480  opthhausdorff0  5481  f1oprswap  6847  wunex2  10698  wuncval2  10707  s4prop  14883  wrdlen2  14917  wwlktovf  14929  wwlktovf1  14930  wwlktovfo  14931  wrd2f1tovbij  14933  prdsval  17425  xpsfval  17536  xpsval  17540  ipoval  18496  frmdval  18785  symg2bas  19330  xpstopnlem2  23705  tusval  24160  tmsval  24376  tmsxpsval  24433  uniiccdif  25486  dchrval  27152  eengv  28913  wkslem1  29542  wkslem2  29543  iswlk  29545  wlkonl1iedg  29600  2wlklem  29602  redwlk  29607  wlkp1lem7  29614  wlkdlem2  29618  upgrwlkdvdelem  29673  usgr2pthlem  29700  usgr2pth  29701  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem6  29752  iswwlks  29773  0enwwlksnge1  29801  wlkiswwlks2lem2  29807  wlkiswwlks2lem5  29810  wwlksm1edg  29818  wwlksnred  29829  wwlksnext  29830  wwlksnredwwlkn  29832  wwlksnextproplem2  29847  2wlkdlem10  29872  umgrwwlks2on  29894  rusgrnumwwlkl1  29905  isclwwlk  29920  clwwlkccatlem  29925  clwwlkccat  29926  clwlkclwwlklem2a1  29928  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlk  29938  clwwisshclwwslemlem  29949  clwwisshclwwslem  29950  clwwisshclwws  29951  clwwlkinwwlk  29976  clwwlkn2  29980  clwwlkel  29982  clwwlkf  29983  clwwlkwwlksb  29990  clwwlkext2edg  29992  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  umgr2cwwk2dif  30000  s2elclwwlknon2  30040  clwwlknonex2lem2  30044  clwwlknonex2  30045  3wlkdlem10  30105  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eupthseg  30142  upgreupthseg  30145  eupth2lem3  30172  nfrgr2v  30208  frgr3vlem1  30209  frgr3vlem2  30210  4cycl2vnunb  30226  disjdifprg  32511  s2rnOLD  32872  idlsrgval  33481  revwlk  35119  kur14lem1  35200  kur14  35210  bj-endval  37310  tgrpfset  40745  tgrpset  40746  hlhilset  41935  dfac21  43062  mendval  43175  oaun2  43377  mnurndlem1  44277  sge0sn  46384  isuspgrimlem  47899  upgrimwlklem5  47905  grtriproplem  47942  isgrtri  47946  grtriclwlk3  47948  cycl3grtrilem  47949  stgrfv  47956  gpgov  48037  gpgprismgriedgdmss  48047  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgedgiov  48060  gpg3kgrtriexlem6  48083  gpg3kgrtriex  48084  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem10  48098  pgnbgreunbgr  48119  isupwlk  48128  zlmodzxzsub  48352  2arymaptf  48645  prelrrx2b  48707  rrx2plordisom  48716  onsetreclem1  49698