Theorem preq12d 4674

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

Syntax hints:   → wi 4   = wceq 1539  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  opeq1  4801  csbopg  4819  opthhausdorff  5425  opthhausdorff0  5426  f1oprswap  6743  wunex2  10425  wuncval2  10434  s4prop  14551  wrdlen2  14585  wwlktovf  14599  wwlktovf1  14600  wwlktovfo  14601  wrd2f1tovbij  14603  prdsval  17083  xpsfval  17194  xpsval  17198  ipoval  18163  frmdval  18405  symg2bas  18915  xpstopnlem2  22870  tusval  23325  tmsval  23542  tmsxpsval  23600  uniiccdif  24647  dchrval  26287  eengv  27250  wkslem1  27877  wkslem2  27878  iswlk  27880  wlkonl1iedg  27935  2wlklem  27937  redwlk  27942  wlkp1lem7  27949  wlkdlem2  27953  upgrwlkdvdelem  28005  usgr2pthlem  28032  usgr2pth  28033  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  iswwlks  28102  0enwwlksnge1  28130  wlkiswwlks2lem2  28136  wlkiswwlks2lem5  28139  wwlksm1edg  28147  wwlksnred  28158  wwlksnext  28159  wwlksnredwwlkn  28161  wwlksnextproplem2  28176  2wlkdlem10  28201  umgrwwlks2on  28223  rusgrnumwwlkl1  28234  isclwwlk  28249  clwwlkccatlem  28254  clwwlkccat  28255  clwlkclwwlklem2a1  28257  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlk  28267  clwwisshclwwslemlem  28278  clwwisshclwwslem  28279  clwwisshclwws  28280  clwwlkinwwlk  28305  clwwlkn2  28309  clwwlkel  28311  clwwlkf  28312  clwwlkwwlksb  28319  clwwlkext2edg  28321  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  umgr2cwwk2dif  28329  s2elclwwlknon2  28369  clwwlknonex2lem2  28373  clwwlknonex2  28374  3wlkdlem10  28434  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eupthseg  28471  upgreupthseg  28474  eupth2lem3  28501  nfrgr2v  28537  frgr3vlem1  28538  frgr3vlem2  28539  4cycl2vnunb  28555  disjdifprg  30815  s2rn  31120  idlsrgval  31550  revwlk  32986  kur14lem1  33068  kur14  33078  bj-endval  35413  tgrpfset  38685  tgrpset  38686  hlhilset  39875  dfac21  40807  mendval  40924  mnurndlem1  41788  sge0sn  43807  isomuspgrlem2b  45169  isupwlk  45186  zlmodzxzsub  45584  2arymaptf  45886  prelrrx2b  45948  rrx2plordisom  45957  onsetreclem1  46296