Theorem preq12d 4694

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  opeq1  4825  csbopg  4843  opthhausdorff  5457  opthhausdorff0  5458  f1oprswap  6807  wunex2  10626  wuncval2  10635  s4prop  14814  wrdlen2  14848  wwlktovf  14860  wwlktovf1  14861  wwlktovfo  14862  wrd2f1tovbij  14864  prdsval  17356  xpsfval  17467  xpsval  17471  ipoval  18433  frmdval  18756  symg2bas  19303  xpstopnlem2  23724  tusval  24178  tmsval  24394  tmsxpsval  24451  uniiccdif  25504  dchrval  27170  eengv  28955  wkslem1  29584  wkslem2  29585  iswlk  29587  wlkonl1iedg  29640  2wlklem  29642  redwlk  29647  wlkp1lem7  29654  wlkdlem2  29658  upgrwlkdvdelem  29712  usgr2pthlem  29739  usgr2pth  29740  crctcshwlkn0lem4  29789  crctcshwlkn0lem5  29790  crctcshwlkn0lem6  29791  iswwlks  29812  0enwwlksnge1  29840  wlkiswwlks2lem2  29846  wlkiswwlks2lem5  29849  wwlksm1edg  29857  wwlksnred  29868  wwlksnext  29869  wwlksnredwwlkn  29871  wwlksnextproplem2  29886  2wlkdlem10  29911  umgrwwlks2on  29933  rusgrnumwwlkl1  29944  isclwwlk  29959  clwwlkccatlem  29964  clwwlkccat  29965  clwlkclwwlklem2a1  29967  clwlkclwwlklem2fv1  29970  clwlkclwwlklem2a4  29972  clwlkclwwlklem2a  29973  clwlkclwwlklem2  29975  clwlkclwwlk  29977  clwwisshclwwslemlem  29988  clwwisshclwwslem  29989  clwwisshclwws  29990  clwwlkinwwlk  30015  clwwlkn2  30019  clwwlkel  30021  clwwlkf  30022  clwwlkwwlksb  30029  clwwlkext2edg  30031  wwlksext2clwwlk  30032  wwlksubclwwlk  30033  umgr2cwwk2dif  30039  s2elclwwlknon2  30079  clwwlknonex2lem2  30083  clwwlknonex2  30084  3wlkdlem10  30144  upgr3v3e3cycl  30155  upgr4cycl4dv4e  30160  eupthseg  30181  upgreupthseg  30184  eupth2lem3  30211  nfrgr2v  30247  frgr3vlem1  30248  frgr3vlem2  30249  4cycl2vnunb  30265  disjdifprg  32550  s2rnOLD  32920  idlsrgval  33463  revwlk  35157  kur14lem1  35238  kur14  35248  bj-endval  37348  tgrpfset  40782  tgrpset  40783  hlhilset  41972  dfac21  43098  mendval  43211  oaun2  43413  mnurndlem1  44313  sge0sn  46416  isuspgrimlem  47925  upgrimwlklem5  47931  grtriproplem  47969  isgrtri  47973  grtriclwlk3  47975  cycl3grtrilem  47976  stgrfv  47983  gpgov  48072  gpgprismgriedgdmss  48082  gpgedgvtx0  48091  gpgedgvtx1  48092  gpgedgiov  48095  gpg3kgrtriexlem6  48118  gpg3kgrtriex  48119  gpgprismgr4cycllem3  48127  gpgprismgr4cycllem10  48134  pgnbgreunbgr  48155  gpg5edgnedg  48160  grlimedgnedg  48161  isupwlk  48166  zlmodzxzsub  48390  2arymaptf  48683  prelrrx2b  48745  rrx2plordisom  48754  onsetreclem1  49736