Theorem preq12d 4746

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

Syntax hints:   → wi 4   = wceq 1537  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  opeq1  4878  csbopg  4896  opthhausdorff  5527  opthhausdorff0  5528  f1oprswap  6893  wunex2  10776  wuncval2  10785  s4prop  14946  wrdlen2  14980  wwlktovf  14992  wwlktovf1  14993  wwlktovfo  14994  wrd2f1tovbij  14996  prdsval  17502  xpsfval  17613  xpsval  17617  ipoval  18588  frmdval  18877  symg2bas  19425  xpstopnlem2  23835  tusval  24290  tmsval  24509  tmsxpsval  24567  uniiccdif  25627  dchrval  27293  eengv  29009  wkslem1  29640  wkslem2  29641  iswlk  29643  wlkonl1iedg  29698  2wlklem  29700  redwlk  29705  wlkp1lem7  29712  wlkdlem2  29716  upgrwlkdvdelem  29769  usgr2pthlem  29796  usgr2pth  29797  crctcshwlkn0lem4  29843  crctcshwlkn0lem5  29844  crctcshwlkn0lem6  29845  iswwlks  29866  0enwwlksnge1  29894  wlkiswwlks2lem2  29900  wlkiswwlks2lem5  29903  wwlksm1edg  29911  wwlksnred  29922  wwlksnext  29923  wwlksnredwwlkn  29925  wwlksnextproplem2  29940  2wlkdlem10  29965  umgrwwlks2on  29987  rusgrnumwwlkl1  29998  isclwwlk  30013  clwwlkccatlem  30018  clwwlkccat  30019  clwlkclwwlklem2a1  30021  clwlkclwwlklem2fv1  30024  clwlkclwwlklem2a4  30026  clwlkclwwlklem2a  30027  clwlkclwwlklem2  30029  clwlkclwwlk  30031  clwwisshclwwslemlem  30042  clwwisshclwwslem  30043  clwwisshclwws  30044  clwwlkinwwlk  30069  clwwlkn2  30073  clwwlkel  30075  clwwlkf  30076  clwwlkwwlksb  30083  clwwlkext2edg  30085  wwlksext2clwwlk  30086  wwlksubclwwlk  30087  umgr2cwwk2dif  30093  s2elclwwlknon2  30133  clwwlknonex2lem2  30137  clwwlknonex2  30138  3wlkdlem10  30198  upgr3v3e3cycl  30209  upgr4cycl4dv4e  30214  eupthseg  30235  upgreupthseg  30238  eupth2lem3  30265  nfrgr2v  30301  frgr3vlem1  30302  frgr3vlem2  30303  4cycl2vnunb  30319  disjdifprg  32595  s2rnOLD  32913  idlsrgval  33511  revwlk  35109  kur14lem1  35191  kur14  35201  bj-endval  37298  tgrpfset  40727  tgrpset  40728  hlhilset  41917  dfac21  43055  mendval  43168  oaun2  43371  mnurndlem1  44277  sge0sn  46335  isuspgrimlem  47812  grtriproplem  47844  isgrtri  47848  grtriclwlk3  47850  stgrfv  47856  gpgov  47937  gpgedgvtx0  47954  gpgedgvtx1  47955  isupwlk  47980  zlmodzxzsub  48205  2arymaptf  48502  prelrrx2b  48564  rrx2plordisom  48573  onsetreclem1  48936