Theorem preq12d 4702

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  opeq1  4833  csbopg  4851  opthhausdorff  5490  opthhausdorff0  5491  f1oprswap  6862  wunex2  10804  wuncval2  10813  s4prop  15041  wrdlen2  15075  wwlktovf  15089  wwlktovf1  15090  wwlktovfo  15091  wrd2f1tovbij  15093  prdsval  17606  xpsfval  17718  xpsval  17722  ipoval  18684  frmdval  19027  symg2bas  19587  xpstopnlem2  24110  tusval  24564  tmsval  24780  tmsxpsval  24837  uniiccdif  25879  dchrval  27543  eengv  29539  wkslem1  30170  wkslem2  30171  iswlk  30173  wlkonl1iedg  30226  2wlklem  30228  redwlk  30233  wlkp1lem7  30240  wlkdlem2  30244  revwlk  30249  upgrwlkdvdelem  30304  usgr2pthlem  30331  usgr2pth  30332  crctcshwlkn0lem4  30384  crctcshwlkn0lem5  30385  crctcshwlkn0lem6  30386  iswwlks  30407  0enwwlksnge1  30435  wlkiswwlks2lem2  30441  wlkiswwlks2lem5  30444  wwlksm1edg  30452  wwlksnred  30463  wwlksnext  30464  wwlksnredwwlkn  30466  wwlksnextproplem2  30481  2wlkdlem10  30506  usgrwwlks2on  30529  umgrwwlks2on  30530  rusgrnumwwlkl1  30542  isclwwlk  30557  clwwlkccatlem  30562  clwwlkccat  30563  clwlkclwwlklem2a1  30565  clwlkclwwlklem2fv1  30568  clwlkclwwlklem2a4  30570  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  clwlkclwwlk  30575  clwwisshclwwslemlem  30586  clwwisshclwwslem  30587  clwwisshclwws  30588  clwwlkinwwlk  30613  clwwlkn2  30617  clwwlkel  30619  clwwlkf  30620  clwwlkwwlksb  30627  clwwlkext2edg  30629  wwlksext2clwwlk  30630  wwlksubclwwlk  30631  umgr2cwwk2dif  30637  s2elclwwlknon2  30677  clwwlknonex2lem2  30681  clwwlknonex2  30682  3wlkdlem10  30752  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  eupthseg  30789  upgreupthseg  30792  eupth2lem3  30819  nfrgr2v  30855  frgr3vlem1  30856  frgr3vlem2  30857  4cycl2vnunb  30873  disjdifprg  33151  idlsrgval  34017  kur14lem1  35940  kur14  35950  bj-endval  38204  tgrpfset  41769  tgrpset  41770  hlhilset  42959  dfac21  44026  mendval  44139  oaun2  44341  mnurndlem1  45224  sge0sn  47333  isuspgrimlem  48937  upgrimwlklem5  48943  grtriproplem  48981  isgrtri  48985  grtriclwlk3  48987  cycl3grtrilem  48988  stgrfv  48995  gpgov  49084  gpgprismgriedgdmss  49094  gpgedgvtx0  49103  gpgedgvtx1  49104  gpgedgiov  49107  gpg3kgrtriexlem6  49130  gpg3kgrtriex  49131  gpgprismgr4cycllem3  49139  gpgprismgr4cycllem10  49146  pgnbgreunbgr  49167  gpg5edgnedg  49172  grlimedgnedg  49173  isupwlk  49178  zlmodzxzsub  49416  2arymaptf  49708  prelrrx2b  49770  rrx2plordisom  49779  onsetreclem1  50742