Theorem preq12d 4703

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

Syntax hints:   → wi 4   = wceq 1563  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  opeq1  4834  csbopg  4852  opthhausdorff  5491  opthhausdorff0  5492  f1oprswap  6856  wunex2  10711  wuncval2  10720  s4prop  14937  wrdlen2  14971  wwlktovf  14983  wwlktovf1  14984  wwlktovfo  14985  wrd2f1tovbij  14987  prdsval  17498  xpsfval  17610  xpsval  17614  ipoval  18576  frmdval  18900  symg2bas  19454  xpstopnlem2  23929  tusval  24383  tmsval  24599  tmsxpsval  24656  uniiccdif  25698  dchrval  27356  eengv  29238  wkslem1  29866  wkslem2  29867  iswlk  29869  wlkonl1iedg  29922  2wlklem  29924  redwlk  29929  wlkp1lem7  29936  wlkdlem2  29940  upgrwlkdvdelem  29994  usgr2pthlem  30021  usgr2pth  30022  crctcshwlkn0lem4  30071  crctcshwlkn0lem5  30072  crctcshwlkn0lem6  30073  iswwlks  30094  0enwwlksnge1  30122  wlkiswwlks2lem2  30128  wlkiswwlks2lem5  30131  wwlksm1edg  30139  wwlksnred  30150  wwlksnext  30151  wwlksnredwwlkn  30153  wwlksnextproplem2  30168  2wlkdlem10  30193  usgrwwlks2on  30216  umgrwwlks2on  30217  rusgrnumwwlkl1  30229  isclwwlk  30244  clwwlkccatlem  30249  clwwlkccat  30250  clwlkclwwlklem2a1  30252  clwlkclwwlklem2fv1  30255  clwlkclwwlklem2a4  30257  clwlkclwwlklem2a  30258  clwlkclwwlklem2  30260  clwlkclwwlk  30262  clwwisshclwwslemlem  30273  clwwisshclwwslem  30274  clwwisshclwws  30275  clwwlkinwwlk  30300  clwwlkn2  30304  clwwlkel  30306  clwwlkf  30307  clwwlkwwlksb  30314  clwwlkext2edg  30316  wwlksext2clwwlk  30317  wwlksubclwwlk  30318  umgr2cwwk2dif  30324  s2elclwwlknon2  30364  clwwlknonex2lem2  30368  clwwlknonex2  30369  3wlkdlem10  30429  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  eupthseg  30466  upgreupthseg  30469  eupth2lem3  30496  nfrgr2v  30532  frgr3vlem1  30533  frgr3vlem2  30534  4cycl2vnunb  30550  disjdifprg  32830  s2rnOLD  33177  idlsrgval  33710  revwlk  35488  kur14lem1  35569  kur14  35579  bj-endval  37819  tgrpfset  41380  tgrpset  41381  hlhilset  42570  dfac21  43655  mendval  43768  oaun2  43970  mnurndlem1  44855  sge0sn  46951  isuspgrimlem  48515  upgrimwlklem5  48521  grtriproplem  48559  isgrtri  48563  grtriclwlk3  48565  cycl3grtrilem  48566  stgrfv  48573  gpgov  48662  gpgprismgriedgdmss  48672  gpgedgvtx0  48681  gpgedgvtx1  48682  gpgedgiov  48685  gpg3kgrtriexlem6  48708  gpg3kgrtriex  48709  gpgprismgr4cycllem3  48717  gpgprismgr4cycllem10  48724  pgnbgreunbgr  48745  gpg5edgnedg  48750  grlimedgnedg  48751  isupwlk  48756  zlmodzxzsub  48991  2arymaptf  49283  prelrrx2b  49345  rrx2plordisom  49354  onsetreclem1  50334