Theorem preq12d 4722

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  opeq1  4854  csbopg  4872  opthhausdorff  5497  opthhausdorff0  5498  f1oprswap  6867  wunex2  10757  wuncval2  10766  s4prop  14934  wrdlen2  14968  wwlktovf  14980  wwlktovf1  14981  wwlktovfo  14982  wrd2f1tovbij  14984  prdsval  17474  xpsfval  17585  xpsval  17589  ipoval  18545  frmdval  18834  symg2bas  19379  xpstopnlem2  23754  tusval  24209  tmsval  24425  tmsxpsval  24482  uniiccdif  25536  dchrval  27202  eengv  28963  wkslem1  29592  wkslem2  29593  iswlk  29595  wlkonl1iedg  29650  2wlklem  29652  redwlk  29657  wlkp1lem7  29664  wlkdlem2  29668  upgrwlkdvdelem  29723  usgr2pthlem  29750  usgr2pth  29751  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  crctcshwlkn0lem6  29802  iswwlks  29823  0enwwlksnge1  29851  wlkiswwlks2lem2  29857  wlkiswwlks2lem5  29860  wwlksm1edg  29868  wwlksnred  29879  wwlksnext  29880  wwlksnredwwlkn  29882  wwlksnextproplem2  29897  2wlkdlem10  29922  umgrwwlks2on  29944  rusgrnumwwlkl1  29955  isclwwlk  29970  clwwlkccatlem  29975  clwwlkccat  29976  clwlkclwwlklem2a1  29978  clwlkclwwlklem2fv1  29981  clwlkclwwlklem2a4  29983  clwlkclwwlklem2a  29984  clwlkclwwlklem2  29986  clwlkclwwlk  29988  clwwisshclwwslemlem  29999  clwwisshclwwslem  30000  clwwisshclwws  30001  clwwlkinwwlk  30026  clwwlkn2  30030  clwwlkel  30032  clwwlkf  30033  clwwlkwwlksb  30040  clwwlkext2edg  30042  wwlksext2clwwlk  30043  wwlksubclwwlk  30044  umgr2cwwk2dif  30050  s2elclwwlknon2  30090  clwwlknonex2lem2  30094  clwwlknonex2  30095  3wlkdlem10  30155  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  eupthseg  30192  upgreupthseg  30195  eupth2lem3  30222  nfrgr2v  30258  frgr3vlem1  30259  frgr3vlem2  30260  4cycl2vnunb  30276  disjdifprg  32561  s2rnOLD  32924  idlsrgval  33523  revwlk  35152  kur14lem1  35233  kur14  35243  bj-endval  37338  tgrpfset  40768  tgrpset  40769  hlhilset  41958  dfac21  43065  mendval  43178  oaun2  43380  mnurndlem1  44280  sge0sn  46388  isuspgrimlem  47888  upgrimwlklem5  47894  grtriproplem  47931  isgrtri  47935  grtriclwlk3  47937  cycl3grtrilem  47938  stgrfv  47945  gpgov  48026  gpgprismgriedgdmss  48036  gpgedgvtx0  48045  gpgedgvtx1  48046  gpg3kgrtriexlem6  48070  gpg3kgrtriex  48071  gpgprismgr4cycllem3  48076  gpgprismgr4cycllem10  48083  isupwlk  48091  zlmodzxzsub  48315  2arymaptf  48612  prelrrx2b  48674  rrx2plordisom  48683  onsetreclem1  49549