Theorem preq12d 4712

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  opeq1  4843  csbopg  4861  opthhausdorff  5505  opthhausdorff0  5506  f1oprswap  6873  wunex2  10741  wuncval2  10750  s4prop  14973  wrdlen2  15007  wwlktovf  15019  wwlktovf1  15020  wwlktovfo  15021  wrd2f1tovbij  15023  prdsval  17533  xpsfval  17645  xpsval  17649  ipoval  18611  frmdval  18941  symg2bas  19494  xpstopnlem2  24005  tusval  24459  tmsval  24675  tmsxpsval  24732  uniiccdif  25774  dchrval  27435  eengv  29366  wkslem1  29994  wkslem2  29995  iswlk  29997  wlkonl1iedg  30050  2wlklem  30052  redwlk  30057  wlkp1lem7  30064  wlkdlem2  30068  upgrwlkdvdelem  30122  usgr2pthlem  30149  usgr2pth  30150  crctcshwlkn0lem4  30199  crctcshwlkn0lem5  30200  crctcshwlkn0lem6  30201  iswwlks  30222  0enwwlksnge1  30250  wlkiswwlks2lem2  30256  wlkiswwlks2lem5  30259  wwlksm1edg  30267  wwlksnred  30278  wwlksnext  30279  wwlksnredwwlkn  30281  wwlksnextproplem2  30296  2wlkdlem10  30321  usgrwwlks2on  30344  umgrwwlks2on  30345  rusgrnumwwlkl1  30357  isclwwlk  30372  clwwlkccatlem  30377  clwwlkccat  30378  clwlkclwwlklem2a1  30380  clwlkclwwlklem2fv1  30383  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwlkclwwlk  30390  clwwisshclwwslemlem  30401  clwwisshclwwslem  30402  clwwisshclwws  30403  clwwlkinwwlk  30428  clwwlkn2  30432  clwwlkel  30434  clwwlkf  30435  clwwlkwwlksb  30442  clwwlkext2edg  30444  wwlksext2clwwlk  30445  wwlksubclwwlk  30446  umgr2cwwk2dif  30452  s2elclwwlknon2  30492  clwwlknonex2lem2  30496  clwwlknonex2  30497  3wlkdlem10  30557  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  eupthseg  30594  upgreupthseg  30597  eupth2lem3  30624  nfrgr2v  30660  frgr3vlem1  30661  frgr3vlem2  30662  4cycl2vnunb  30678  disjdifprg  32957  idlsrgval  33824  revwlk  35638  kur14lem1  35719  kur14  35729  bj-endval  38000  tgrpfset  41559  tgrpset  41560  hlhilset  42749  dfac21  43834  mendval  43947  oaun2  44149  mnurndlem1  45032  sge0sn  47134  isuspgrimlem  48701  upgrimwlklem5  48707  grtriproplem  48745  isgrtri  48749  grtriclwlk3  48751  cycl3grtrilem  48752  stgrfv  48759  gpgov  48848  gpgprismgriedgdmss  48858  gpgedgvtx0  48867  gpgedgvtx1  48868  gpgedgiov  48871  gpg3kgrtriexlem6  48894  gpg3kgrtriex  48895  gpgprismgr4cycllem3  48903  gpgprismgr4cycllem10  48910  pgnbgreunbgr  48931  gpg5edgnedg  48936  grlimedgnedg  48937  isupwlk  48942  zlmodzxzsub  49181  2arymaptf  49473  prelrrx2b  49535  rrx2plordisom  49544  onsetreclem1  50524