Theorem preq12d 4699

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

Syntax hints:   → wi 4   = wceq 1559  {cpr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4582  df-pr 4584

This theorem is referenced by:  opeq1  4830  csbopg  4848  opthhausdorff  5485  opthhausdorff0  5486  f1oprswap  6848  wunex2  10693  wuncval2  10702  s4prop  14920  wrdlen2  14954  wwlktovf  14966  wwlktovf1  14967  wwlktovfo  14968  wrd2f1tovbij  14970  prdsval  17467  xpsfval  17579  xpsval  17583  ipoval  18545  frmdval  18868  symg2bas  19416  xpstopnlem2  23851  tusval  24305  tmsval  24521  tmsxpsval  24578  uniiccdif  25620  dchrval  27275  eengv  29126  wkslem1  29754  wkslem2  29755  iswlk  29757  wlkonl1iedg  29810  2wlklem  29812  redwlk  29817  wlkp1lem7  29824  wlkdlem2  29828  upgrwlkdvdelem  29882  usgr2pthlem  29909  usgr2pth  29910  crctcshwlkn0lem4  29959  crctcshwlkn0lem5  29960  crctcshwlkn0lem6  29961  iswwlks  29982  0enwwlksnge1  30010  wlkiswwlks2lem2  30016  wlkiswwlks2lem5  30019  wwlksm1edg  30027  wwlksnred  30038  wwlksnext  30039  wwlksnredwwlkn  30041  wwlksnextproplem2  30056  2wlkdlem10  30081  usgrwwlks2on  30104  umgrwwlks2on  30105  rusgrnumwwlkl1  30117  isclwwlk  30132  clwwlkccatlem  30137  clwwlkccat  30138  clwlkclwwlklem2a1  30140  clwlkclwwlklem2fv1  30143  clwlkclwwlklem2a4  30145  clwlkclwwlklem2a  30146  clwlkclwwlklem2  30148  clwlkclwwlk  30150  clwwisshclwwslemlem  30161  clwwisshclwwslem  30162  clwwisshclwws  30163  clwwlkinwwlk  30188  clwwlkn2  30192  clwwlkel  30194  clwwlkf  30195  clwwlkwwlksb  30202  clwwlkext2edg  30204  wwlksext2clwwlk  30205  wwlksubclwwlk  30206  umgr2cwwk2dif  30212  s2elclwwlknon2  30252  clwwlknonex2lem2  30256  clwwlknonex2  30257  3wlkdlem10  30317  upgr3v3e3cycl  30328  upgr4cycl4dv4e  30333  eupthseg  30354  upgreupthseg  30357  eupth2lem3  30384  nfrgr2v  30420  frgr3vlem1  30421  frgr3vlem2  30422  4cycl2vnunb  30438  disjdifprg  32724  s2rnOLD  33083  idlsrgval  33660  revwlk  35439  kur14lem1  35520  kur14  35530  bj-endval  37771  tgrpfset  41332  tgrpset  41333  hlhilset  42522  dfac21  43607  mendval  43720  oaun2  43922  mnurndlem1  44821  sge0sn  46917  isuspgrimlem  48481  upgrimwlklem5  48487  grtriproplem  48525  isgrtri  48529  grtriclwlk3  48531  cycl3grtrilem  48532  stgrfv  48539  gpgov  48628  gpgprismgriedgdmss  48638  gpgedgvtx0  48647  gpgedgvtx1  48648  gpgedgiov  48651  gpg3kgrtriexlem6  48674  gpg3kgrtriex  48675  gpgprismgr4cycllem3  48683  gpgprismgr4cycllem10  48690  pgnbgreunbgr  48711  gpg5edgnedg  48716  grlimedgnedg  48717  isupwlk  48722  zlmodzxzsub  48946  2arymaptf  49238  prelrrx2b  49300  rrx2plordisom  49309  onsetreclem1  50290