Theorem preq12d 4698

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  opeq1  4839  csbopg  4850  opthhausdorff  5489  opthhausdorff0  5490  f1oprswap  6870  wunex2  10826  wuncval2  10835  s4prop  15066  wrdlen2  15100  wwlktovf  15114  wwlktovf1  15115  wwlktovfo  15116  wrd2f1tovbij  15118  prdsval  17631  xpsfval  17743  xpsval  17747  ipoval  18709  frmdval  19052  symg2bas  19612  xpstopnlem2  24135  tusval  24589  tmsval  24805  tmsxpsval  24862  uniiccdif  25904  dchrval  27566  eengv  29562  wkslem1  30193  wkslem2  30194  iswlk  30196  wlkonl1iedg  30249  2wlklem  30251  redwlk  30256  wlkp1lem7  30263  wlkdlem2  30267  revwlk  30272  upgrwlkdvdelem  30327  usgr2pthlem  30354  usgr2pth  30355  crctcshwlkn0lem4  30407  crctcshwlkn0lem5  30408  crctcshwlkn0lem6  30409  iswwlks  30430  0enwwlksnge1  30458  wlkiswwlks2lem2  30464  wlkiswwlks2lem5  30467  wwlksm1edg  30475  wwlksnred  30486  wwlksnext  30487  wwlksnredwwlkn  30489  wwlksnextproplem2  30504  2wlkdlem10  30529  usgrwwlks2on  30552  umgrwwlks2on  30553  rusgrnumwwlkl1  30565  isclwwlk  30580  clwwlkccatlem  30585  clwwlkccat  30586  clwlkclwwlklem2a1  30588  clwlkclwwlklem2fv1  30591  clwlkclwwlklem2a4  30593  clwlkclwwlklem2a  30594  clwlkclwwlklem2  30596  clwlkclwwlk  30598  clwwisshclwwslemlem  30609  clwwisshclwwslem  30610  clwwisshclwws  30611  clwwlkinwwlk  30636  clwwlkn2  30640  clwwlkel  30642  clwwlkf  30643  clwwlkwwlksb  30650  clwwlkext2edg  30652  wwlksext2clwwlk  30653  wwlksubclwwlk  30654  umgr2cwwk2dif  30660  s2elclwwlknon2  30700  clwwlknonex2lem2  30704  clwwlknonex2  30705  3wlkdlem10  30775  upgr3v3e3cycl  30786  upgr4cycl4dv4e  30791  eupthseg  30812  upgreupthseg  30815  eupth2lem3  30842  nfrgr2v  30878  frgr3vlem1  30879  frgr3vlem2  30880  4cycl2vnunb  30896  disjdifprg  33216  idlsrgval  34081  kur14lem1  36057  kur14  36067  bj-endval  38329  tgrpfset  41894  tgrpset  41895  hlhilset  43084  dfac21  44161  mendval  44274  oaun2  44476  mnurndlem1  45358  sge0sn  47482  isuspgrimlem  49086  upgrimwlklem5  49092  grtriproplem  49130  isgrtri  49134  grtriclwlk3  49136  cycl3grtrilem  49137  stgrfv  49144  gpgov  49233  gpgprismgriedgdmss  49243  gpgedgvtx0  49252  gpgedgvtx1  49253  gpgedgiov  49256  gpg3kgrtriexlem6  49279  gpg3kgrtriex  49280  gpgprismgr4cycllem3  49288  gpgprismgr4cycllem10  49295  pgnbgreunbgr  49316  gpg5edgnedg  49321  grlimedgnedg  49322  isupwlk  49327  zlmodzxzsub  49565  2arymaptf  49857  onsetreclem1  50966