Theorem preq12d 4680

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

Syntax hints:   → wi 4   = wceq 1547  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  opeq1  4811  csbopg  4829  opthhausdorff  5465  opthhausdorff0  5466  f1oprswap  6819  wunex2  10659  wuncval2  10668  s4prop  14870  wrdlen2  14904  wwlktovf  14916  wwlktovf1  14917  wwlktovfo  14918  wrd2f1tovbij  14920  prdsval  17416  xpsfval  17528  xpsval  17532  ipoval  18494  frmdval  18817  symg2bas  19366  xpstopnlem2  23801  tusval  24255  tmsval  24471  tmsxpsval  24528  uniiccdif  25570  dchrval  27222  eengv  29073  wkslem1  29701  wkslem2  29702  iswlk  29704  wlkonl1iedg  29757  2wlklem  29759  redwlk  29764  wlkp1lem7  29771  wlkdlem2  29775  upgrwlkdvdelem  29829  usgr2pthlem  29856  usgr2pth  29857  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  crctcshwlkn0lem6  29908  iswwlks  29929  0enwwlksnge1  29957  wlkiswwlks2lem2  29963  wlkiswwlks2lem5  29966  wwlksm1edg  29974  wwlksnred  29985  wwlksnext  29986  wwlksnredwwlkn  29988  wwlksnextproplem2  30003  2wlkdlem10  30028  usgrwwlks2on  30051  umgrwwlks2on  30052  rusgrnumwwlkl1  30064  isclwwlk  30079  clwwlkccatlem  30084  clwwlkccat  30085  clwlkclwwlklem2a1  30087  clwlkclwwlklem2fv1  30090  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwlkclwwlk  30097  clwwisshclwwslemlem  30108  clwwisshclwwslem  30109  clwwisshclwws  30110  clwwlkinwwlk  30135  clwwlkn2  30139  clwwlkel  30141  clwwlkf  30142  clwwlkwwlksb  30149  clwwlkext2edg  30151  wwlksext2clwwlk  30152  wwlksubclwwlk  30153  umgr2cwwk2dif  30159  s2elclwwlknon2  30199  clwwlknonex2lem2  30203  clwwlknonex2  30204  3wlkdlem10  30264  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eupthseg  30301  upgreupthseg  30304  eupth2lem3  30331  nfrgr2v  30367  frgr3vlem1  30368  frgr3vlem2  30369  4cycl2vnunb  30385  disjdifprg  32671  s2rnOLD  33030  idlsrgval  33593  revwlk  35360  kur14lem1  35441  kur14  35451  bj-endval  37682  tgrpfset  41243  tgrpset  41244  hlhilset  42433  dfac21  43518  mendval  43631  oaun2  43833  mnurndlem1  44732  sge0sn  46829  isuspgrimlem  48393  upgrimwlklem5  48399  grtriproplem  48437  isgrtri  48441  grtriclwlk3  48443  cycl3grtrilem  48444  stgrfv  48451  gpgov  48540  gpgprismgriedgdmss  48550  gpgedgvtx0  48559  gpgedgvtx1  48560  gpgedgiov  48563  gpg3kgrtriexlem6  48586  gpg3kgrtriex  48587  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem10  48602  pgnbgreunbgr  48623  gpg5edgnedg  48628  grlimedgnedg  48629  isupwlk  48634  zlmodzxzsub  48858  2arymaptf  49150  prelrrx2b  49212  rrx2plordisom  49221  onsetreclem1  50202