Theorem preq12d 4708

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

Syntax hints:   → wi 4   = wceq 1570  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  opeq1  4839  csbopg  4857  opthhausdorff  5502  opthhausdorff0  5503  f1oprswap  6868  wunex2  10724  wuncval2  10733  s4prop  14949  wrdlen2  14983  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  wrd2f1tovbij  14999  prdsval  17509  xpsfval  17621  xpsval  17625  ipoval  18587  frmdval  18911  symg2bas  19464  xpstopnlem2  23949  tusval  24403  tmsval  24619  tmsxpsval  24676  uniiccdif  25718  dchrval  27376  eengv  29307  wkslem1  29935  wkslem2  29936  iswlk  29938  wlkonl1iedg  29991  2wlklem  29993  redwlk  29998  wlkp1lem7  30005  wlkdlem2  30009  upgrwlkdvdelem  30063  usgr2pthlem  30090  usgr2pth  30091  crctcshwlkn0lem4  30140  crctcshwlkn0lem5  30141  crctcshwlkn0lem6  30142  iswwlks  30163  0enwwlksnge1  30191  wlkiswwlks2lem2  30197  wlkiswwlks2lem5  30200  wwlksm1edg  30208  wwlksnred  30219  wwlksnext  30220  wwlksnredwwlkn  30222  wwlksnextproplem2  30237  2wlkdlem10  30262  usgrwwlks2on  30285  umgrwwlks2on  30286  rusgrnumwwlkl1  30298  isclwwlk  30313  clwwlkccatlem  30318  clwwlkccat  30319  clwlkclwwlklem2a1  30321  clwlkclwwlklem2fv1  30324  clwlkclwwlklem2a4  30326  clwlkclwwlklem2a  30327  clwlkclwwlklem2  30329  clwlkclwwlk  30331  clwwisshclwwslemlem  30342  clwwisshclwwslem  30343  clwwisshclwws  30344  clwwlkinwwlk  30369  clwwlkn2  30373  clwwlkel  30375  clwwlkf  30376  clwwlkwwlksb  30383  clwwlkext2edg  30385  wwlksext2clwwlk  30386  wwlksubclwwlk  30387  umgr2cwwk2dif  30393  s2elclwwlknon2  30433  clwwlknonex2lem2  30437  clwwlknonex2  30438  3wlkdlem10  30498  upgr3v3e3cycl  30509  upgr4cycl4dv4e  30514  eupthseg  30535  upgreupthseg  30538  eupth2lem3  30565  nfrgr2v  30601  frgr3vlem1  30602  frgr3vlem2  30603  4cycl2vnunb  30619  disjdifprg  32898  s2rnOLD  33242  idlsrgval  33771  revwlk  35595  kur14lem1  35676  kur14  35686  bj-endval  37937  tgrpfset  41496  tgrpset  41497  hlhilset  42686  dfac21  43773  mendval  43886  oaun2  44088  mnurndlem1  44971  sge0sn  47073  isuspgrimlem  48637  upgrimwlklem5  48643  grtriproplem  48681  isgrtri  48685  grtriclwlk3  48687  cycl3grtrilem  48688  stgrfv  48695  gpgov  48784  gpgprismgriedgdmss  48794  gpgedgvtx0  48803  gpgedgvtx1  48804  gpgedgiov  48807  gpg3kgrtriexlem6  48830  gpg3kgrtriex  48831  gpgprismgr4cycllem3  48839  gpgprismgr4cycllem10  48846  pgnbgreunbgr  48867  gpg5edgnedg  48872  grlimedgnedg  48873  isupwlk  48878  zlmodzxzsub  49117  2arymaptf  49409  prelrrx2b  49471  rrx2plordisom  49480  onsetreclem1  50460