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 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  opeq1  4843  csbopg  4854  opthhausdorff  5494  opthhausdorff0  5495  f1oprswap  6893  wunex2  10850  wuncval2  10859  s4prop  15090  wrdlen2  15124  wwlktovf  15138  wwlktovf1  15139  wwlktovfo  15140  wrd2f1tovbij  15142  prdsval  17655  xpsfval  17767  xpsval  17771  ipoval  18733  frmdval  19076  symg2bas  19637  xpstopnlem2  24160  tusval  24614  tmsval  24830  tmsxpsval  24887  uniiccdif  25929  dchrval  27591  eengv  29587  wkslem1  30218  wkslem2  30219  iswlk  30221  wlkonl1iedg  30274  2wlklem  30276  redwlk  30281  wlkp1lem7  30288  wlkdlem2  30292  revwlk  30297  upgrwlkdvdelem  30352  usgr2pthlem  30379  usgr2pth  30380  crctcshwlkn0lem4  30432  crctcshwlkn0lem5  30433  crctcshwlkn0lem6  30434  iswwlks  30455  0enwwlksnge1  30483  wlkiswwlks2lem2  30489  wlkiswwlks2lem5  30492  wwlksm1edg  30500  wwlksnred  30511  wwlksnext  30512  wwlksnredwwlkn  30514  wwlksnextproplem2  30529  2wlkdlem10  30554  usgrwwlks2on  30577  umgrwwlks2on  30578  rusgrnumwwlkl1  30590  isclwwlk  30605  clwwlkccatlem  30610  clwwlkccat  30611  clwlkclwwlklem2a1  30613  clwlkclwwlklem2fv1  30616  clwlkclwwlklem2a4  30618  clwlkclwwlklem2a  30619  clwlkclwwlklem2  30621  clwlkclwwlk  30623  clwwisshclwwslemlem  30634  clwwisshclwwslem  30635  clwwisshclwws  30636  clwwlkinwwlk  30661  clwwlkn2  30665  clwwlkel  30667  clwwlkf  30668  clwwlkwwlksb  30675  clwwlkext2edg  30677  wwlksext2clwwlk  30678  wwlksubclwwlk  30679  umgr2cwwk2dif  30685  s2elclwwlknon2  30725  clwwlknonex2lem2  30729  clwwlknonex2  30730  3wlkdlem10  30800  upgr3v3e3cycl  30811  upgr4cycl4dv4e  30816  eupthseg  30837  upgreupthseg  30840  eupth2lem3  30867  nfrgr2v  30903  frgr3vlem1  30904  frgr3vlem2  30905  4cycl2vnunb  30921  disjdifprg  33241  idlsrgval  34105  kur14lem1  36138  kur14  36148  bj-endval  38428  tgrpfset  41993  tgrpset  41994  hlhilset  43183  dfac21  44261  mendval  44373  oaun2  44575  mnurndlem1  45457  sge0sn  47594  isuspgrimlem  49198  upgrimwlklem5  49204  grtriproplem  49242  isgrtri  49246  grtriclwlk3  49248  cycl3grtrilem  49249  stgrfv  49256  gpgov  49345  gpgprismgriedgdmss  49355  gpgedgvtx0  49364  gpgedgvtx1  49365  gpgedgiov  49368  gpg3kgrtriexlem6  49391  gpg3kgrtriex  49392  gpgprismgr4cycllem3  49400  gpgprismgr4cycllem10  49407  pgnbgreunbgr  49428  gpg5edgnedg  49433  grlimedgnedg  49434  isupwlk  49439  zlmodzxzsub  49677  2arymaptf  49969  onsetreclem1  51078