Theorem preq12d 4710

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

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

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 4593  df-pr 4595

This theorem is used by:  opeq1  4841  csbopg  4859  opthhausdorff  5503  opthhausdorff0  5504  f1oprswap  6870  wunex2  10733  wuncval2  10742  s4prop  14958  wrdlen2  14992  wwlktovf  15004  wwlktovf1  15005  wwlktovfo  15006  wrd2f1tovbij  15008  prdsval  17518  xpsfval  17630  xpsval  17634  ipoval  18596  frmdval  18920  symg2bas  19473  xpstopnlem2  23983  tusval  24437  tmsval  24653  tmsxpsval  24710  uniiccdif  25752  dchrval  27413  eengv  29344  wkslem1  29972  wkslem2  29973  iswlk  29975  wlkonl1iedg  30028  2wlklem  30030  redwlk  30035  wlkp1lem7  30042  wlkdlem2  30046  upgrwlkdvdelem  30100  usgr2pthlem  30127  usgr2pth  30128  crctcshwlkn0lem4  30177  crctcshwlkn0lem5  30178  crctcshwlkn0lem6  30179  iswwlks  30200  0enwwlksnge1  30228  wlkiswwlks2lem2  30234  wlkiswwlks2lem5  30237  wwlksm1edg  30245  wwlksnred  30256  wwlksnext  30257  wwlksnredwwlkn  30259  wwlksnextproplem2  30274  2wlkdlem10  30299  usgrwwlks2on  30322  umgrwwlks2on  30323  rusgrnumwwlkl1  30335  isclwwlk  30350  clwwlkccatlem  30355  clwwlkccat  30356  clwlkclwwlklem2a1  30358  clwlkclwwlklem2fv1  30361  clwlkclwwlklem2a4  30363  clwlkclwwlklem2a  30364  clwlkclwwlklem2  30366  clwlkclwwlk  30368  clwwisshclwwslemlem  30379  clwwisshclwwslem  30380  clwwisshclwws  30381  clwwlkinwwlk  30406  clwwlkn2  30410  clwwlkel  30412  clwwlkf  30413  clwwlkwwlksb  30420  clwwlkext2edg  30422  wwlksext2clwwlk  30423  wwlksubclwwlk  30424  umgr2cwwk2dif  30430  s2elclwwlknon2  30470  clwwlknonex2lem2  30474  clwwlknonex2  30475  3wlkdlem10  30535  upgr3v3e3cycl  30546  upgr4cycl4dv4e  30551  eupthseg  30572  upgreupthseg  30575  eupth2lem3  30602  nfrgr2v  30638  frgr3vlem1  30639  frgr3vlem2  30640  4cycl2vnunb  30656  disjdifprg  32935  idlsrgval  33806  revwlk  35629  kur14lem1  35710  kur14  35720  bj-endval  37991  tgrpfset  41550  tgrpset  41551  hlhilset  42740  dfac21  43825  mendval  43938  oaun2  44140  mnurndlem1  45023  sge0sn  47125  isuspgrimlem  48692  upgrimwlklem5  48698  grtriproplem  48736  isgrtri  48740  grtriclwlk3  48742  cycl3grtrilem  48743  stgrfv  48750  gpgov  48839  gpgprismgriedgdmss  48849  gpgedgvtx0  48858  gpgedgvtx1  48859  gpgedgiov  48862  gpg3kgrtriexlem6  48885  gpg3kgrtriex  48886  gpgprismgr4cycllem3  48894  gpgprismgr4cycllem10  48901  pgnbgreunbgr  48922  gpg5edgnedg  48927  grlimedgnedg  48928  isupwlk  48933  zlmodzxzsub  49172  2arymaptf  49464  prelrrx2b  49526  rrx2plordisom  49535  onsetreclem1  50515