Theorem preq12d 4705

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  opeq1  4836  csbopg  4854  opthhausdorff  5498  opthhausdorff0  5499  f1oprswap  6867  wunex2  10751  wuncval2  10760  s4prop  14985  wrdlen2  15019  wwlktovf  15033  wwlktovf1  15034  wwlktovfo  15035  wrd2f1tovbij  15037  prdsval  17546  xpsfval  17658  xpsval  17662  ipoval  18624  frmdval  18966  symg2bas  19526  xpstopnlem2  24043  tusval  24497  tmsval  24713  tmsxpsval  24770  uniiccdif  25812  dchrval  27478  eengv  29444  wkslem1  30075  wkslem2  30076  iswlk  30078  wlkonl1iedg  30131  2wlklem  30133  redwlk  30138  wlkp1lem7  30145  wlkdlem2  30149  revwlk  30154  upgrwlkdvdelem  30209  usgr2pthlem  30236  usgr2pth  30237  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  crctcshwlkn0lem6  30291  iswwlks  30312  0enwwlksnge1  30340  wlkiswwlks2lem2  30346  wlkiswwlks2lem5  30349  wwlksm1edg  30357  wwlksnred  30368  wwlksnext  30369  wwlksnredwwlkn  30371  wwlksnextproplem2  30386  2wlkdlem10  30411  usgrwwlks2on  30434  umgrwwlks2on  30435  rusgrnumwwlkl1  30447  isclwwlk  30462  clwwlkccatlem  30467  clwwlkccat  30468  clwlkclwwlklem2a1  30470  clwlkclwwlklem2fv1  30473  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwlkclwwlk  30480  clwwisshclwwslemlem  30491  clwwisshclwwslem  30492  clwwisshclwws  30493  clwwlkinwwlk  30518  clwwlkn2  30522  clwwlkel  30524  clwwlkf  30525  clwwlkwwlksb  30532  clwwlkext2edg  30534  wwlksext2clwwlk  30535  wwlksubclwwlk  30536  umgr2cwwk2dif  30542  s2elclwwlknon2  30582  clwwlknonex2lem2  30586  clwwlknonex2  30587  3wlkdlem10  30657  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  eupthseg  30694  upgreupthseg  30697  eupth2lem3  30724  nfrgr2v  30760  frgr3vlem1  30761  frgr3vlem2  30762  4cycl2vnunb  30778  disjdifprg  33056  idlsrgval  33921  kur14lem1  35793  kur14  35803  bj-endval  38075  tgrpfset  41625  tgrpset  41626  hlhilset  42815  dfac21  43915  mendval  44028  oaun2  44230  mnurndlem1  45113  sge0sn  47215  isuspgrimlem  48819  upgrimwlklem5  48825  grtriproplem  48863  isgrtri  48867  grtriclwlk3  48869  cycl3grtrilem  48870  stgrfv  48877  gpgov  48966  gpgprismgriedgdmss  48976  gpgedgvtx0  48985  gpgedgvtx1  48986  gpgedgiov  48989  gpg3kgrtriexlem6  49012  gpg3kgrtriex  49013  gpgprismgr4cycllem3  49021  gpgprismgr4cycllem10  49028  pgnbgreunbgr  49049  gpg5edgnedg  49054  grlimedgnedg  49055  isupwlk  49060  zlmodzxzsub  49298  2arymaptf  49590  prelrrx2b  49652  rrx2plordisom  49661  onsetreclem1  50639