Theorem preq12d 4705

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  opeq1  4837  csbopg  4855  opthhausdorff  5477  opthhausdorff0  5478  f1oprswap  6844  wunex2  10691  wuncval2  10700  s4prop  14876  wrdlen2  14910  wwlktovf  14922  wwlktovf1  14923  wwlktovfo  14924  wrd2f1tovbij  14926  prdsval  17418  xpsfval  17529  xpsval  17533  ipoval  18489  frmdval  18778  symg2bas  19323  xpstopnlem2  23698  tusval  24153  tmsval  24369  tmsxpsval  24426  uniiccdif  25479  dchrval  27145  eengv  28906  wkslem1  29535  wkslem2  29536  iswlk  29538  wlkonl1iedg  29593  2wlklem  29595  redwlk  29600  wlkp1lem7  29607  wlkdlem2  29611  upgrwlkdvdelem  29666  usgr2pthlem  29693  usgr2pth  29694  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  iswwlks  29766  0enwwlksnge1  29794  wlkiswwlks2lem2  29800  wlkiswwlks2lem5  29803  wwlksm1edg  29811  wwlksnred  29822  wwlksnext  29823  wwlksnredwwlkn  29825  wwlksnextproplem2  29840  2wlkdlem10  29865  umgrwwlks2on  29887  rusgrnumwwlkl1  29898  isclwwlk  29913  clwwlkccatlem  29918  clwwlkccat  29919  clwlkclwwlklem2a1  29921  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlk  29931  clwwisshclwwslemlem  29942  clwwisshclwwslem  29943  clwwisshclwws  29944  clwwlkinwwlk  29969  clwwlkn2  29973  clwwlkel  29975  clwwlkf  29976  clwwlkwwlksb  29983  clwwlkext2edg  29985  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  umgr2cwwk2dif  29993  s2elclwwlknon2  30033  clwwlknonex2lem2  30037  clwwlknonex2  30038  3wlkdlem10  30098  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupthseg  30135  upgreupthseg  30138  eupth2lem3  30165  nfrgr2v  30201  frgr3vlem1  30202  frgr3vlem2  30203  4cycl2vnunb  30219  disjdifprg  32504  s2rnOLD  32865  idlsrgval  33474  revwlk  35112  kur14lem1  35193  kur14  35203  bj-endval  37303  tgrpfset  40738  tgrpset  40739  hlhilset  41928  dfac21  43055  mendval  43168  oaun2  43370  mnurndlem1  44270  sge0sn  46377  isuspgrimlem  47895  upgrimwlklem5  47901  grtriproplem  47938  isgrtri  47942  grtriclwlk3  47944  cycl3grtrilem  47945  stgrfv  47952  gpgov  48033  gpgprismgriedgdmss  48043  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgedgiov  48056  gpg3kgrtriexlem6  48079  gpg3kgrtriex  48080  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem10  48094  pgnbgreunbgr  48115  isupwlk  48124  zlmodzxzsub  48348  2arymaptf  48641  prelrrx2b  48703  rrx2plordisom  48712  onsetreclem1  49694