Theorem preq12d 4698

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  opeq1  4829  csbopg  4847  opthhausdorff  5465  opthhausdorff0  5466  f1oprswap  6819  wunex2  10649  wuncval2  10658  s4prop  14833  wrdlen2  14867  wwlktovf  14879  wwlktovf1  14880  wwlktovfo  14881  wrd2f1tovbij  14883  prdsval  17375  xpsfval  17487  xpsval  17491  ipoval  18453  frmdval  18776  symg2bas  19322  xpstopnlem2  23755  tusval  24209  tmsval  24425  tmsxpsval  24482  uniiccdif  25535  dchrval  27201  eengv  29052  wkslem1  29681  wkslem2  29682  iswlk  29684  wlkonl1iedg  29737  2wlklem  29739  redwlk  29744  wlkp1lem7  29751  wlkdlem2  29755  upgrwlkdvdelem  29809  usgr2pthlem  29836  usgr2pth  29837  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  iswwlks  29909  0enwwlksnge1  29937  wlkiswwlks2lem2  29943  wlkiswwlks2lem5  29946  wwlksm1edg  29954  wwlksnred  29965  wwlksnext  29966  wwlksnredwwlkn  29968  wwlksnextproplem2  29983  2wlkdlem10  30008  usgrwwlks2on  30031  umgrwwlks2on  30032  rusgrnumwwlkl1  30044  isclwwlk  30059  clwwlkccatlem  30064  clwwlkccat  30065  clwlkclwwlklem2a1  30067  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlk  30077  clwwisshclwwslemlem  30088  clwwisshclwwslem  30089  clwwisshclwws  30090  clwwlkinwwlk  30115  clwwlkn2  30119  clwwlkel  30121  clwwlkf  30122  clwwlkwwlksb  30129  clwwlkext2edg  30131  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  umgr2cwwk2dif  30139  s2elclwwlknon2  30179  clwwlknonex2lem2  30183  clwwlknonex2  30184  3wlkdlem10  30244  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eupthseg  30281  upgreupthseg  30284  eupth2lem3  30311  nfrgr2v  30347  frgr3vlem1  30348  frgr3vlem2  30349  4cycl2vnunb  30365  disjdifprg  32650  s2rnOLD  33026  idlsrgval  33584  revwlk  35319  kur14lem1  35400  kur14  35410  bj-endval  37516  tgrpfset  41000  tgrpset  41001  hlhilset  42190  dfac21  43304  mendval  43417  oaun2  43619  mnurndlem1  44518  sge0sn  46619  isuspgrimlem  48137  upgrimwlklem5  48143  grtriproplem  48181  isgrtri  48185  grtriclwlk3  48187  cycl3grtrilem  48188  stgrfv  48195  gpgov  48284  gpgprismgriedgdmss  48294  gpgedgvtx0  48303  gpgedgvtx1  48304  gpgedgiov  48307  gpg3kgrtriexlem6  48330  gpg3kgrtriex  48331  gpgprismgr4cycllem3  48339  gpgprismgr4cycllem10  48346  pgnbgreunbgr  48367  gpg5edgnedg  48372  grlimedgnedg  48373  isupwlk  48378  zlmodzxzsub  48602  2arymaptf  48894  prelrrx2b  48956  rrx2plordisom  48965  onsetreclem1  49946